proposition: Lemma Grammaire2' : isGram X V2' R2' S2'.
proof: Proof. rewrite <- egal_X_X2'. unfold X2', V2', R2', S2', GGG2, GG2, G2 in |- *. apply image_isGram. auto. change (Mots X2') in |- *. rewrite egal_X_X2'. auto. apply inter_Xim_Vim_empty; auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4