proposition: Theorem equiv_APD_Gram : l_egal (LA X wd wa d) (LG X V R S').
proof: Proof. red in |- *. unfold l_inclus, LA, LG in |- *. split. intros w temp; elim temp; intros Der inmon. auto. intros w temp; elim temp; intros Der inmon. auto. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata