proposition: Theorem wf_strict_order_finite : well_founded R.
proof: Proof. Proof using HX Rirrefl Rtrans. destruct HX as (m & Hm). apply wf_strict_order_list with (m := m); auto. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(wf_chains)