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