proposition: Lemma map_eq_injective: forall {A B: Type} (f: A->B) (pinj: injective_fun f) (lvi lvo: list A), map f lvi = map f lvo -> lvi = lvo.
proof: Proof. induction lvi as [| vi lvi Hind]; introv Hm; destruct lvo; (try invertsn Hm); auto. apply pinj in Hm. f_equal; auto. Qed.
imports: UsefulTypes bin_rels Omega