proposition: Lemma two_maps_map2 : forall {A A1 A2 B} f1 f2 f aa, (@map2 A1 A2 B f (@map A _ f1 aa) (@map A _ f2 aa)) = map (fun x => f (f1 x) (f2 x)) aa.
proof: Proof. intros; unfold map2; rewrite zip2_maps_same, map_map; reflexivity. Qed.
imports: List