proposition: Lemma in_zip2_map_map_eq : forall {A B A' fa fb a b aa bb}, @map A A' fa aa = @map B A' fb bb -> In (a, b) (@zip2 A B aa bb) -> fa a = fb b.
proof: Proof. intros; match goal with | [ H: map ?f ?l = map ?g ?l', H': In _ (zip2 ?l ?l') |- _ ] => apply (in_zip2_map f g) in H'; rewrite <- H, zip2_maps_same, in_map_iff in H'; firstorder congruence end. Qed.
imports: List Program