proposition: Lemma Derivestar_P_A_2_imp_Derivestar_P_A : forall x y : Word * Word, Derivestar_P_A_2 x y -> Derivestar_P_A X d x y.
proof: Proof. unfold Derivestar_P_A_2, Rstar, Derivestar_P_A in |- *. intros x y Rstar_Der. pattern x, y in |- *. apply Rstar_Der. intros. apply Rstar_reflexive. intros u v w Hyp1 Hyp2. apply Rstar_R with v; auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata