proposition: Lemma nodup_complete (lst : plist A) (H : pNoDup lst) : nodup lst = true.
proof: Proof. induction lst. + constructor. + simpl in *. rewrite andb_true_iff. inversion H; subst; split; clear H. * apply eq_true_not_negb. intros H; apply H2. apply inb_sound; assumption. * 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