proposition: Lemma rev_inj : forall l1 l2, rev l1 = rev l2 -> l1 = l2.
proof: Proof. Proof using. introv E. forwards E': f_equal (@rev A) (rm E). do 2 rewrite~ rev_rev in E'. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)