proposition: Lemma map2_two_maps: forall {A B A' B' C} fa fb g aa bb, @map2 A B C (fun a b => g (fa a) (fb b)) aa bb = @map2 A' B' C (fun a b => g a b) (map fa aa) (map fb bb).
proof: Proof. unfold map2; 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