proposition: Lemma map_fst_zip2' {A1 A2 B}: forall {f: _ -> B} {aa1 aa2}, Datatypes.length aa1 = Datatypes.length aa2 -> map (fun x => f (fst x)) (@zip2 A1 A2 aa1 aa2) = map f aa1.
proof: Proof. induction aa1; destruct aa2; map_length_t. Qed.
imports: List