proposition: Lemma egal_LG : Id X f -> l_egal (LG X V R S) (LG Xim Vim Rim Sim).
proof: Proof. unfold l_egal in |- *. intro Id_X. unfold l_inclus in |- *. split. intros w LG_X_w. replace w with (wef w). unfold Sim, Rim, Gim3, Vim, Gim2, Xim, Gim, wef in |- *. auto. apply (Id_words_inv X). prolog [ LG_inv ] 2. exact (extension_Id X f Id_X). intros w LG_Xim_w. replace X with Xim'. replace V with Vim'. replace S with Sim'. replace R with Rim'. replace w with (weinvf (wef w)). unfold Sim', Rim', Gim3', Vim', Gim2', Xim', Gim', weinvf in |- *. apply Reconnait_imageGram. replace (wef w) with w. assumption. apply sym_equal. apply (Id_words_inv X). rewrite <- (egal_Xim Id_X). prolog [ LG_inv ] 2. exact (extension_Id X f Id_X). pattern w at 2 in |- *; replace w with (comp_word weinvf wef w). apply refl_equal. apply Id_words_inv with (union X V). apply inmonoid_inclus with X. auto. replace X with Xim. prolog [ LG_inv ] 2. exact (egal_Xim Id_X). exact weinvf_wef. exact egalR. exact egalS. exact egalV. exact egalX. Qed.
imports: Ensf Words more_words need fonctions Relations gram gram2