proposition: Lemma chain_bounded n x y : chain R n x y -> n <= length m.
proof: Proof. Proof using Hm Rirrefl Rtrans. intros H. destruct (le_lt_dec n (length m)) as [ | C ]; auto. destruct chain_chain_list with (1 := H) as (ll & H1 & H2). cut (list_has_dup ll). + intros H3. apply list_has_dup_equiv in H3 as (z & l & u & r & ->). apply chain_list_app_inv in H1 as (a & _ & H1). apply chain_list_cons_inv in H1 as (<- & k & H3 & H1). apply chain_list_app_inv in H1 as (p & H4 & H1). apply chain_list_cons_inv in H1 as (<- & _ & _ & _). apply chain_list_chain in H4. destruct (@chain_irrefl (length u) z). constructor 2 with k; auto. + apply chain_list_incl in H1. apply finite_php_dup with (2 := H1); lia. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(wf_chains)