proposition: Theorem wf_strict_order_list : well_founded R.
proof: Proof. Proof using Hm Rirrefl Rtrans. apply wf_chains; eauto. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(wf_chains)