proposition: Lemma map_inj : forall f l1 l2, (forall x y, f x = f y -> x = y) -> map f l1 = map f l2 -> l1 = l2.
proof: Proof. Proof using. intros f l1. induction l1; introv I E. { rewrite map_nil in E. forwards*: map_eq_nil_inv. } { destruct l2 as [|b l2]; tryfalse. do 2 rewrite map_cons in E. inverts E. fequals*. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)