proposition: Lemma map2_fst {A1 A2}: forall {aa1 aa2}, Datatypes.length aa1 = Datatypes.length aa2 -> @map2 A1 A2 _ (fun x y => x) aa1 aa2 = aa1.
proof: Proof. unfold map2; induction aa1; destruct aa2; map_length_t. Qed.
imports: List