[STATEMENT]
lemma szip_sconst_smap_fst: "sconst a ||| xs = smap (Pair a) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconst a ||| xs = smap (Pair a) xs
[PROOF STEP]
by (coinduction arbitrary: xs) (auto)