proposition: Lemma discrete_nodup X (L : list X) : eq_dec X -> { L' | NoDup L' /\ incl L L' }.
proof: Proof. intros d. induction L. - exists nil. split; [|easy]. apply NoDup_nil. - destruct IHL as (L' & H1 & H2). decide (a el L') as [H|H]. + exists L'. split; trivial. intros b. cbn. firstorder congruence. + exists (cons a L'). split; try now apply NoDup_cons. auto using incl_cons, in_eq, incl_tl. Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List Undecidability.Synthetic.Definitions