proposition: Theorem wf_sincl : well_founded sincl.
proof: Proof. apply wf_chains. intros l; exists (length l). intros ? ?; apply sincl_chain_bounded. Qed.
imports: Arith List Wellfounded Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(acc_irr measure_ind wf_chains)