proposition: Lemma Reconnait_imageGram_iso : forall w : Word, inmonoid X w -> LG Xim Vim Rim Sim (wef w) -> LG X V R S w.
proof: Proof. intros w inmonoid_X_w LG_wef_w. rewrite <- egalR. rewrite <- egalS. rewrite <- egalV. rewrite <- egalX. replace w with (weinvf (wef w)). unfold Sim', Rim', Gim3', Vim', Gim2', Xim', Gim', weinvf in |- *. auto. change (comp_word weinvf wef w = w :>Word) in |- *. apply Id_words_inv with X. assumption. apply Id_words_inclus with (union X V). auto. exact weinvf_wef. Qed.
imports: Ensf Words more_words need fonctions Relations gram gram2