proposition: Lemma map_eq_cons_inv : forall f l1 (x2:B) t2, map f l1 = x2::t2 -> exists x1 t1, l1 = x1::t1 /\ x2 = f x1 /\ t2 = map f t1.
proof: Proof. Proof using. introv E. destruct l1; [false|]. rewrite map_cons in E. inverts* E. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)