fst package:sbv

fst :: (SymVal a, SymVal b) => STuple a b -> SBV a

First of a tuple

fst3 :: (SymVal a, SymVal b, SymVal c) => STuple3 a b c -> SBV a

First of a 3-tuple

sbv Documentation.SBV.Examples.KnuckleDragger.Lists

length xs = length ys ⟹ map fst (zip xs ys) = xs

>>> map_fst_zip
Inductive lemma: map_fst_zip
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Result:                               Q.E.D.
[Proven] map_fst_zip

map_fst_zip_take :: IO Proof

sbv Documentation.SBV.Examples.KnuckleDragger.Lists

map fst (zip xs ys) = take (min (length xs) (length ys)) xs

>>> map_fst_zip_take
Lemma: take_cons                        Q.E.D.
Inductive lemma: map_fst_zip_take
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Result:                               Q.E.D.
[Proven] map_fst_zip_take