proposition: Lemma X_P_wd_wa_d : P_automata X P wd wa d.
proof: Proof. red in |- *. split. unfold wd in |- *. apply inmonoid_cons. trivial. unfold P in |- *. apply union_d. apply isGram3 with X R. exact Gram. split. apply inmonoid_nil. exact Trans. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata