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