proposition: Lemma cut2_cons_N : forall (A : Elt) (v : Word), ~ dans A X -> cut2 (cons A v) = cons A v.
proof: Proof. intros A v N_dans_A_X. unfold cut2, cut in |- *. elim (cut_spec (cons A v)). intros a temp; elim temp; clear temp. intros b temp; elim temp; clear temp. intros inmon_a temp; elim temp; clear temp. intros App_eg spec_or. cut (inmonoid X a). cut (Append a b = cons A v). clear App_eg inmon_a. generalize a; clear a; simple induction a. auto. intros x w Hyp App_eg_x_w inmon. absurd (dans A X). assumption. replace A with x. apply inmonoid_cons_inv2 with w. assumption. apply cons_cons_inv1 with (Append w b) v. assumption. assumption. assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata