proposition: Lemma Grammaire1' : isGram X V1' R1' S1'.
proof: Proof. rewrite <- egal_X_X1'. unfold X1', V1', R1', S1', GGG1, GG1, G1 in |- *. apply image_isGram. auto. change (Mots X1') in |- *. rewrite egal_X_X1'. auto. apply inter_Xim_Vim_empty; auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4