proposition: Lemma NoDup_rev l : NoDup l -> NoDup (rev l).
proof: Proof. induction l as [|a l IHl]; simpl; intros Hnd; [ constructor | ]. inversion_clear Hnd as [ | ? ? Hnin Hndl ]. assert (Add a (rev l) (rev l ++ a :: nil)) as Hadd by (rewrite <- (app_nil_r (rev l)) at 1; apply Add_app). apply NoDup_Add in Hadd; apply Hadd; intuition. now apply Hnin, in_rev. Qed.
imports: PeanoNat