proposition: Fact chain_list_incl l x y : chain_list R l x y -> l ⊆ m.
proof: Proof. Proof using Hm. induction 1; simpl; eauto. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(wf_chains)