proposition: Theorem Derivestar_imp_Derivestar_P_A : forall x y : Word, Derivestar R x y -> inmonoid X y -> Derivestar_P_A X d (x, y) (nil, nil).
proof: Proof. auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata