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