proposition: Lemma nodup_In l x : In x (nodup l) <-> In x l.
proof: Proof. induction l as [|a l' Hrec]; simpl. - reflexivity. - destruct (in_dec decA a l'); simpl; rewrite Hrec. * now intuition subst. * reflexivity. Qed.
imports: PeanoNat