proposition: Lemma rincl_fin_chains n m l : chain rincl_fin n m l -> exists ll, ~ list_has_dup ll /\ incl ll M /\ length ll = n /\ incl ll m.
proof: Proof. induction 1 as [ x | n m k l H1 H2 (ll & H3 & H4 & H5 & H6) ]. + exists nil. repeat split; simpl; auto; inversion 1. + destruct H1 as (H1 & a & G1 & G2 & G3). exists (a::ll). repeat split. * contradict H3. apply list_has_dup_cons_inv in H3. destruct H3 as [ H3 | ]; auto. destruct G1; apply H6; auto. * apply incl_cons; auto. * simpl; f_equal; auto. * apply incl_cons; auto. intros ? ?; auto. Qed.
imports: Arith List Wellfounded Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(acc_irr measure_ind wf_chains)