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