proposition: Lemma Derivestar_P_A_2_x : forall x : Word, inmonoid X x -> Derivestar_P_A_2 (x, x) (nil, nil).
proof: Proof. unfold Derivestar_P_A_2 in |- *. simple induction x. intro. apply Rstar_reflexive. intros x0 w Hyp inmon. apply Rstar_R with (w, w). apply Derive_X. apply inmonoid_cons_inv2 with w; assumption. apply Hyp. apply inmonoid_cons_inv with x0; assumption. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata