proposition: Corollary rincl_fin_chain_bounded l m n : chain rincl_fin n m l -> n <= length M.
proof: Proof. intros H. apply rincl_fin_chains in H. destruct H as (ll & H1 & H2 & H3 & _). destruct (le_lt_dec n (length M)) as [ | C ]; auto. subst n; destruct H1. apply finite_php_dup with M; auto. Qed.
imports: Arith List Wellfounded Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(acc_irr measure_ind wf_chains)