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