proposition: Lemma wf_strict_incl: well_founded (@strict_incl X).
proof: Proof. Proof using D. eapply well_founded_lt_compat with (f := fun A => length (nodup eq_dec A)). intros A B [H [x [H1 H2]]]. assert (nodup eq_dec A ⊆ nodup eq_dec B) as H3 by now rewrite !nodup_seteq. eapply NoDup_incl_length in H3 as H4; [| eapply NoDup_nodup]. eapply Nat.lt_eq_cases in H4 as []; eauto; exfalso. eapply NoDup_length_incl in H3. rewrite !nodup_seteq in H3; intuition (auto with datatypes). eapply NoDup_nodup. lia. Qed.
imports: List Arith Lia Morphisms FinFun Init.Wf Undecidability.HOU(std.decidable)