proposition: Lemma nodup_sound (lst : plist A) (H : nodup lst = true) : pNoDup lst.
proof: Proof. induction lst. + constructor. + simpl in *. rewrite andb_true_iff in H; destruct H as [H1 H2]. rewrite negb_true_iff in H1. constructor. * intro H. apply inb_complete in H. intuition congruence. * apply IHlst; assumption. Qed.
imports: ExtLib.Structures.Functor ExtLib.Structures.Applicative ExtLib.Data.POption ExtLib.Data.PPair ExtLib.Core.RelDec ExtLib.Tactics.Consider ExtLib.Tactics.Injection Coq.Bool.Bool