length xs == length ys ==> map snd (zip xs ys) = xs
>>> runTP $ map_snd_zip @Integer @Integer 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 :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
map snd (zip xs ys) == take (min (length xs) (length ys)) xs
>>> runTP $ map_snd_zip_take @Integer @Integer 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 :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool