snd package:sbv

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

Second of a tuple

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

Second of a 3-tuple

sbv Documentation.SBV.Examples.KnuckleDragger.Lists

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

>>> map_snd_zip
Inductive lemma: map_snd_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_snd_zip

map_snd_zip_take :: IO Proof

sbv Documentation.SBV.Examples.KnuckleDragger.Lists

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

>>> map_snd_zip_take
Lemma: take_cons                        Q.E.D.
Inductive lemma: map_snd_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_snd_zip_take