proposition: Lemma in_zip2 : forall {A B} a b aa bb, In (a, b) (@zip2 A B aa bb) -> (In a aa /\ In b bb).
proof: Proof. induction aa; destruct bb; repeat match goal with | _ => progress simpl | _ => progress intuition | [ H: _ = _ |- _ ] => inversion_clear H | [ aa: list ?a, H: forall _: list ?a, _ |- _ ] => specialize (H aa) end. Qed.
imports: List