(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 gram2.v                                  *)
(****************************************************************************)
(*              Formal Language Theory                                      *)
(*                                                                          *)
(*              Judicael Courant - Jean-Christophe Filliatre                *)
(*                                                                          *)
(*              Developped in V5.8  June-July 1993                          *)
(*              Ported     to V5.10 October 1994                            *)
(****************************************************************************)

Require Import Ensf.
Require Import Words.
Require Import more_words.
Require Import need.
Require Import fonctions.
Require Import Relations.
Require Import gram.

Hint Resolve extension_Id.
Section resultats.


Variable X V1 R1 : Ensf.
Variable S1 : Elt.
Variable V2 R2 : Ensf.
Variable S2 : Elt.

Let C := Gunion V1 R1 V2 R2.
Let Vu := fst C.
Let Ru := snd C.


Lemma inter_X_Vu : isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> inter X Vu empty.
(* Goal: forall (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2), inter X Vu empty *)
intro G1.
(* Goal: forall _ : isGram X V2 R2 S2, inter X Vu empty *)
intro G2.
(* Goal: inter X Vu empty *)
unfold Vu in |- *.
(* Goal: inter X (@fst Ensf Ensf C) empty *)
unfold C in |- *.
(* Goal: inter X (@fst Ensf Ensf (Gunion V1 R1 V2 R2)) empty *)
unfold Gunion in |- *.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
simpl in |- *.
(* Goal: inter X (union V1 V2) empty *)
apply union_inter.
(* Goal: inter X V1 empty *)
(* Goal: inter X V2 empty *)
apply isGram2 with R1 S1; assumption.
(* Goal: inter X V2 empty *)
(* Goal: inter V1 V2 empty *)
(* Goal: Derive Ru u v *)
(* Goal: inmonoid (union X V1) u *)
(* Goal: inmonoid (union X V1) u *)
apply isGram2 with R2 S2; assumption.
Qed.


Lemma Gunion_Regles :
 isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> Regles X Vu Ru.
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R1 u v) (_ : Derive Rim (wef u) (wef v)), Derive Rim (wef (cons x u)) (wef (cons x v)) *)
intros.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
unfold Ru in |- *; unfold C in |- *; unfold Gunion in |- *; simpl in |- *.
apply Regles_union; unfold Vu in |- *; unfold C in |- *;
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
 unfold Gunion in |- *; simpl in |- *.
apply Regles_V with V1;
 [ auto | apply isGram4 with S1; auto ].
apply Regles_V with V2;
 [ auto | apply isGram4 with S2; auto ].
Qed.


Lemma inmon_Der_imp_Der :
 Regles X V1 R1 ->
 Regles X V2 R2 ->
 inter (union X V1) V2 empty ->
 forall u v : Word, Derive Ru u v -> inmonoid (union X V1) u -> Derive R1 u v.
(* Goal: forall (_ : Regles X V1 R1) (_ : Regles X V2 R2) (_ : inter (union X V1) V2 empty) (u v : Word) (_ : Derive Ru u v) (_ : inmonoid (union X V1) u), Derive R1 u v *)
intros Re_1 Re_2 inter_X_V1_V2_empty u v Der_Ru_u.
(* Goal: forall _ : inmonoid (union X V2) u, Derive R2 u v *)
elim Der_Ru_u.
(* Goal: forall (u v : Word) (A : Elt) (_ : dans (couple A (word u)) Ru) (_ : inmonoid (union X V2) (cons A v)), Derive R2 (cons A v) (Append u v) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	intros u0 v0 A dans_couple_Ru inmon_cons_A_v0.
(* Goal: Derive R2 (cons A v0) (Append u0 v0) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	apply Derive1.
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	cut (dans (couple A (word u0)) R1 \/ dans (couple A (word u0)) R2). (**)
(* Goal: forall _ : @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
	intro temp; elim temp; clear temp.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		auto.

(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R1 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
		intro dans_R2.
(* Goal: dans (couple A (word u0)) R1 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
		absurd (inter (union X V1) V2 empty).
(* Goal: not (inter (union X V2) V1 empty) *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			red in |- *.
(* Goal: forall _ : inter (union X V2) V1 empty, False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			unfold inter in |- *.
(* Goal: forall _ : @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
			intro temp; elim temp; clear temp.
(* Goal: forall (_ : inclus empty (union X V1)) (_ : and (inclus empty V2) (forall (x : Elt) (_ : dans x (union X V1)) (_ : dans x V2), dans x empty)), False *)
(* Goal: inter (union X V1) V2 empty *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
			intros incl_empty_X_V1 temp; elim temp; clear temp.
(* Goal: forall (_ : inclus empty V2) (_ : forall (x : Elt) (_ : dans x (union X V1)) (_ : dans x V2), dans x empty), False *)
(* Goal: inter (union X V1) V2 empty *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
			intros incl_empty_V2 imp.
(* Goal: False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			apply dans_empty_imp_P with A.
(* Goal: Derive R1 u0 v0 *)
			apply imp.
(* Goal: dans A (union X V1) *)
(* Goal: dans A V2 *)
(* Goal: inter (union X V1) V2 empty *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
				apply inmonoid_cons_inv2 with v0; assumption.
(* Goal: dans A V2 *)
(* Goal: inter (union X V1) V2 empty *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
				apply Regles_inv1 with X R2 (word u0); assumption.

(* Goal: Id (union X (add a V1')) f *)
		assumption.

(* Goal: Id (union X (add a V1')) f *)
	(**) apply dans_union; assumption.

(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) u, Derive R1 u v) (_ : inmonoid (union X V1) (cons x u)), Derive R1 (cons x u) (cons x v) *)
	intros u0 v0 x Der_Ru imp inmon_cons_x_u0.
(* Goal: Derive R1 (cons x u0) (cons x v0) *)
	apply Derive2.
(* Goal: Derive R1 u0 v0 *)
	apply imp.
(* Goal: inmonoid (union X V1) u0 *)
	apply inmonoid_cons_inv with x.
(* Goal: Id (union X (add a V1')) f *)
	assumption.
Qed.


Lemma inmon_Der_imp_inmon_R1 :
 forall u v : Word,
 Regles X V1 R1 ->
 Derive R1 u v -> inmonoid (union X V1) u -> inmonoid (union X V1) v.
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R1 u v) (_ : Derive Rim (wef u) (wef v)), Derive Rim (wef (cons x u)) (wef (cons x v)) *)
intros.
(* Goal: Id (union X (add a V1')) f *)
apply in_mon_X_Der_imp_inmon_X with R1 u; assumption.
Qed.

Lemma inmon_Der_imp_inmon :
 forall u v : Word,
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 inmonoid (union X V1) u -> Derive Ru u v -> inmonoid (union X V1) v.
(* Goal: forall (u v : Word) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty) (_ : inmonoid (union X V1) u) (_ : Derive Ru u v), inmonoid (union X V1) v *)
intros u v G_R1 G_R2 inter_V1_V2_empty inmon_X_V1_u Der_Ru_u_v.
(* Goal: inmonoid (union X V1) v *)
apply inmon_Der_imp_inmon_R1 with u.
(* Goal: Id (union X (add a V1')) f *)
	apply isGram4 with S1; assumption.

(* Goal: Derive R1 u v *)
(* Goal: inmonoid (union X V1) u *)
	apply inmon_Der_imp_Der.
(* Goal: Id (union X (add a V1')) f *)
		apply isGram4 with S1; assumption.

(* Goal: Id (union X (add a V1')) f *)
		apply isGram4 with S2; assumption.

(* Goal: inter (union X V1) V2 empty *)
(* Goal: Derive Ru u v *)
(* Goal: inmonoid (union X V1) u *)
(* Goal: inmonoid (union X V1) u *)
		apply inter_union.
(* Goal: inter X V2 empty *)
(* Goal: inter V1 V2 empty *)
(* Goal: Derive Ru u v *)
(* Goal: inmonoid (union X V1) u *)
(* Goal: inmonoid (union X V1) u *)
			apply isGram2 with R2 S2; assumption.
(* Goal: Id (union X (add a V1')) f *)
			assumption.

(* Goal: Id (union X (add a V1')) f *)
		assumption.

(* Goal: Id (union X (add a V1')) f *)
		assumption.

(* Goal: Id (union X (add a V1')) f *)
	assumption.

Qed.

Lemma Gunion_Derivestar :
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 forall u v : Word,
 Derivestar Ru u v -> inmonoid (union X V1) u -> Derivestar R1 u v.
(* Goal: forall (u v : Word) (_ : Derivestar R1 u v), Derivestar Rim (wef u) (wef v) *)
unfold Derivestar in |- *.
(* Goal: forall (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty) (u v : Word) (_ : Rstar Word (Derive Ru) u v) (_ : inmonoid (union X V2) u), Rstar Word (Derive R2) u v *)
intros G_1 G_2 inter_V1_V2_empty u v Derivestar_Ru.
(* Goal: Rstar Word (Derive Rim) (wef u) (wef v) *)
pattern u, v in |- *.
(* Goal: (fun w w0 : Word => forall _ : inmonoid (union X V2) w, Rstar Word (Derive R2) w w0) u v *)
apply Derivestar_Ru.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	auto. (*Intros.
	Apply Rstar_reflexive.*)

(* Goal: forall (u v w : Word) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V1) v, Rstar Word (Derive R1) v w) (_ : inmonoid (union X V1) u), Rstar Word (Derive R1) u w *)
	intros u0 v0 w Der_Ru inmon_v0_imp_Rstar_R1_v0 inmon_u0. 
(*Prolog [Rstar_R inmon_Der_imp_Der isGram4  inter_union  isGram2 inmon_Der_imp_inmon ] 6. -> raisonnable seulement sur Cray...*)
(* Goal: Rstar Word (Derive R2) u0 w *)
	apply Rstar_R with v0.
(* Goal: Derive R1 u0 v0 *)
(* Goal: Rstar Word (Derive R1) v0 w *)
		prolog [ inmon_Der_imp_Der isGram4 inter_union isGram2 ] 5.
(*		Apply inmon_Der_imp_Der.
			Apply isGram4 with S1;Assumption.
			Apply isGram4 with S2;Assumption.
			Apply inter_union.
				Apply isGram2 with R2 S2; Assumption.
				Assumption.
			Assumption.
			Assumption.*)

(* Goal: Rstar Word (Derive R1) v0 w *)
		prolog [ inmon_Der_imp_inmon ] 3.
(*		Apply inmon_v0_imp_Rstar_R1_v0.
		Apply inmon_Der_imp_inmon with u0;Assumption.*)

Qed.


Lemma inmon_Der_imp_Der2 :
 Regles X V1 R1 ->
 Regles X V2 R2 ->
 inter (union X V2) V1 empty ->
 forall u v : Word, Derive Ru u v -> inmonoid (union X V2) u -> Derive R2 u v.
(* Goal: forall (_ : Regles X V1 R1) (_ : Regles X V2 R2) (_ : inter (union X V2) V1 empty) (u v : Word) (_ : Derive Ru u v) (_ : inmonoid (union X V2) u), Derive R2 u v *)
intros Re_1 Re_2 inter_X_V2_V1_empty u v Der_Ru_u.
(* Goal: forall _ : inmonoid (union X V2) u, Derive R2 u v *)
elim Der_Ru_u.
(* Goal: forall (u v : Word) (A : Elt) (_ : dans (couple A (word u)) Ru) (_ : inmonoid (union X V2) (cons A v)), Derive R2 (cons A v) (Append u v) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	intros u0 v0 A dans_couple_Ru inmon_cons_A_v0.
(* Goal: Derive R2 (cons A v0) (Append u0 v0) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	apply Derive1.
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	cut (dans (couple A (word u0)) R1 \/ dans (couple A (word u0)) R2). (**)
(* Goal: forall _ : @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
	intro temp; elim temp; clear temp.
(* Goal: forall _ : dans (couple A (word u0)) R1, dans (couple A (word u0)) R2 *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
		intro dans_R1.
(* Goal: dans (couple A (word u0)) R2 *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
		absurd (inter (union X V2) V1 empty).
(* Goal: not (inter (union X V2) V1 empty) *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			red in |- *.
(* Goal: forall _ : inter (union X V2) V1 empty, False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
			unfold inter in |- *.
(* Goal: forall _ : and (inclus empty (union X V2)) (and (inclus empty V1) (forall (x : Elt) (_ : dans x (union X V2)) (_ : dans x V1), dans x empty)), False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
intros (H1, (H2, H3)).
			(* Intuition. *)
		        (*Intros;*)
(* Goal: False *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
apply dans_empty_imp_P with A.

(* Goal: dans A empty *)
(* Goal: inter (union X V2) V1 empty *)
(* Goal: forall _ : dans (couple A (word u0)) R2, dans (couple A (word u0)) R2 *)
(* Goal: or (dans (couple A (word u0)) R1) (dans (couple A (word u0)) R2) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
prolog [ inmonoid_cons_inv2 Regles_inv1 ] 3.
(*			Intros incl_empty_V1 imp incl_empty_X_V2.*)


(*			Apply dans_empty_imp_P with A.
			Apply imp.
				Apply inmonoid_cons_inv2 with v0;Assumption.
				Apply Regles_inv1 with X R1 (word u0);
						Assumption.
*)
(* Goal: Id (union X (add a V1')) f *)
		assumption.

(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	trivial.

(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	(**) auto.

(* Goal: forall (u v : Word) (x : Elt) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) u, Derive R2 u v) (_ : inmonoid (union X V2) (cons x u)), Derive R2 (cons x u) (cons x v) *)
	prolog [ Derive2 inmonoid_cons_inv ] 10.
(*	Intros u0 v0 x Der_Ru imp inmon_cons_x_u0.
	Apply Derive2.
	Apply imp.
	Apply inmonoid_cons_inv with x.
	Assumption.*)
Qed.

Lemma inmon_Der_imp_inmon_R2 :
 forall u v : Word,
 Regles X V2 R2 ->
 Derive R2 u v -> inmonoid (union X V2) u -> inmonoid (union X V2) v.
(* Goal: forall (u v : Word) (_ : Regles X V2 R2) (_ : Derive R2 u v) (_ : inmonoid (union X V2) u), inmonoid (union X V2) v *)
intros u v Regles_R2 Der_R2.
(* Goal: forall _ : inmonoid (union X V2) u, inmonoid (union X V2) v *)
elim Der_R2.
(* Goal: forall (u v : Word) (A : Elt) (_ : dans (couple A (word u)) R2) (_ : inmonoid (union X V2) (cons A v)), inmonoid (union X V2) (Append u v) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R2 u v) (_ : forall _ : inmonoid (union X V2) u, inmonoid (union X V2) v) (_ : inmonoid (union X V2) (cons x u)), inmonoid (union X V2) (cons x v) *)
	intros; prolog [ inmonoid_cons_inv Regles_inv2 inmonoid_Append ] 3.
(*	Intros u0 v0 A dans_R2 inmonoid_cons_A_v0.
	Apply inmonoid_Append.
		Apply Regles_inv2 with R2 A;Assumption.
		Apply inmonoid_cons_inv with A; Assumption.*)

(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R2 u v) (_ : forall _ : inmonoid (union X V2) u, inmonoid (union X V2) v) (_ : inmonoid (union X V2) (cons x u)), inmonoid (union X V2) (cons x v) *)
	intros; prolog [ inmonoid_cons_inv2 inmonoid_cons_inv inmonoid_cons ] 4.
	(*Intros u0 v0 x Der_R2_u0 imp inmon_cons_x_u0.
	Apply inmonoid_cons.
		Apply imp.
		Apply inmonoid_cons_inv with x;Assumption.

		Apply inmonoid_cons_inv2 with u0;Assumption.*)

Qed.

Lemma inmon_Der_imp_inmon_2 :
 forall u v : Word,
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 inmonoid (union X V2) u -> Derive Ru u v -> inmonoid (union X V2) v.
(* with Prolog...*)
intros;
 prolog
  [ inmon_Der_imp_inmon_R2 sym_inter isGram2 inter_union isGram4
   inmon_Der_imp_Der2 ] 5.

(* without Prolog...*)
(*Intros u v G_R1 G_R2 inter_V1_V2_empty inmon_X_V2_u Der_Ru_u_v.
Apply inmon_Der_imp_inmon_R2 with u.
	Apply isGram4 with S2;Assumption.

	
	Apply inmon_Der_imp_Der2.
		Apply isGram4 with S1;Assumption.

		Apply isGram4 with S2;Assumption.

		Apply inter_union.
			Apply isGram2 with R1 S1; Assumption.
			Apply sym_inter; Assumption.

		Assumption.

		Assumption.

	Assumption.*)
Qed.

Lemma Gunion_Derivestar2 :
 isGram X V1 R1 S1 ->
 isGram X V2 R2 S2 ->
 inter V1 V2 empty ->
 forall u v : Word,
 Derivestar Ru u v -> inmonoid (union X V2) u -> Derivestar R2 u v.
(* Goal: forall (u v : Word) (_ : Derivestar R1 u v), Derivestar Rim (wef u) (wef v) *)
unfold Derivestar in |- *.
(* Goal: forall (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : inter V1 V2 empty) (u v : Word) (_ : Rstar Word (Derive Ru) u v) (_ : inmonoid (union X V2) u), Rstar Word (Derive R2) u v *)
intros G_1 G_2 inter_V1_V2_empty u v Derivestar_Ru.
(* Goal: Rstar Word (Derive Rim) (wef u) (wef v) *)
pattern u, v in |- *.
(* Goal: (fun w w0 : Word => forall _ : inmonoid (union X V2) w, Rstar Word (Derive R2) w w0) u v *)
apply Derivestar_Ru.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	auto. (*Intros.
	Apply Rstar_reflexive.*)

(* Goal: forall (u v w : Word) (_ : Derive Ru u v) (_ : forall _ : inmonoid (union X V2) v, Rstar Word (Derive R2) v w) (_ : inmonoid (union X V2) u), Rstar Word (Derive R2) u w *)
	intros u0 v0 w Der_Ru inmon_v0_imp_Rstar_R2_v0 inmon_u0. 
(* Goal: Rstar Word (Derive R2) u0 w *)
	apply Rstar_R with v0.
(* Goal: Derive R2 u0 v0 *)
(* Goal: Rstar Word (Derive R2) v0 w *)
		prolog [ sym_inter isGram2 inter_union isGram4 inmon_Der_imp_Der2 ] 4.
		(*Apply inmon_Der_imp_Der2.
			Apply isGram4 with S1;Assumption.
			Apply isGram4 with S2;Assumption.
			Apply inter_union.
				Apply isGram2 with R1 S1; Assumption.
				Apply sym_inter;Assumption.
			Assumption.
			Assumption.*)

(* Goal: Rstar Word (Derive R2) v0 w *)
		prolog [ inmon_Der_imp_inmon_2 ] 3.
		(*Apply inmon_v0_imp_Rstar_R2_v0.
		Apply inmon_Der_imp_inmon_2 with u0;Assumption.*)
Qed.


Lemma Gunion_isGram :
 forall S : Elt,
 isGram X V1 R1 S1 -> isGram X V2 R2 S2 -> dans S Vu -> isGram X Vu Ru S.

(* Goal: forall (S : Elt) (_ : isGram X V1 R1 S1) (_ : isGram X V2 R2 S2) (_ : dans S Vu), isGram X Vu Ru S *)
prolog [ isGram5 isGram1 inter_X_Vu Gunion_Regles ] 7.

(*Intros.
Apply isGram5.

Apply isGram1 with V1 R1 S1 ; Assumption.

Apply inter_X_Vu ; Assumption.

Assumption.

Apply Gunion_Regles; Assumption.*)

Qed.


Variable f : Elt -> Elt.

Let wef := Word_ext f.
Let fet (w : Elt) := word (wef (word_inv w)).
Let fonc (P : Elt) := couple (f (first P)) (fet (second P)).


Let Gim := imageGram f X V1 R1 S1.
Let Xim := fst Gim.
Let Gim2 := snd Gim.
Let Vim := fst Gim2.
Let Gim3 := snd Gim2.
Let Rim := fst Gim3.
Let Sim := snd Gim3.

Lemma dans_Rim :
 forall (A : Elt) (u : Word),
 dans (couple A (word u)) R1 -> dans (couple (f A) (word (wef u))) Rim.
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R1 u v) (_ : Derive Rim (wef u) (wef v)), Derive Rim (wef (cons x u)) (wef (cons x v)) *)
intros.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
unfold Rim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *.
replace (couple (f A) (word (wef u))) with (fonc (couple A (word u)));
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
 auto.
Qed.
Hint Resolve dans_Rim.

Lemma image_Regles : Regles X V1 R1 -> Regles Xim Vim Rim.
unfold Rim, Vim, Xim, Gim3, Gim2, Gim, imageGram, Regles in |- *;
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
 simpl in |- *.
(* Goal: forall (_ : forall (x : Elt) (_ : dans x R1), @ex2 Elt (fun A : Elt => dans A V1) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union X V1) B))) (x : Elt) (_ : dans x (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R1)), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
intros R_R1 x dans_x.
(* Goal: @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
cut (exists x_ant : Elt, dans x_ant R1 /\ x = fonc x_ant :>Elt).
(* Goal: forall _ : @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
intro temp; elim temp; clear temp.
(* Goal: forall (x0 : Elt) (_ : and (dans x0 R1) (@eq Elt x (fonc x0))), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
intros x_ant temp; elim temp; clear temp; intros x_ant_in_R1 x_egal.
(* Goal: @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
elim (R_R1 x_ant x_ant_in_R1).
(* Goal: forall (x0 : Elt) (_ : dans x0 V1) (_ : @ex2 Word (fun B : Word => @eq Elt x_ant (couple x0 (word B))) (fun B : Word => inmonoid (union X V1) B)), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
intros A_ant dans_A_ant_V1 temp; elim temp; clear temp.
(* Goal: forall (x0 : Word) (_ : @eq Elt x_ant (couple A_ant (word x0))) (_ : inmonoid (union X V1) x0), @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
intros B_ant x_ant_egal inmonoid_x_ant.
(* Goal: @ex2 Elt (fun A : Elt => dans A (map f V1)) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B)) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
exists (f A_ant).
(* Goal: Id (union X (add a V1')) f *)
	apply dans_map_inv; assumption.
(* Goal: @ex2 Word (fun B : Word => @eq Elt x (couple (f A_ant) (word B))) (fun B : Word => inmonoid (union (map f X) (map f V1)) B) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
	exists (Word_ext f B_ant).
(* Goal: @eq Elt x (couple (f A_ant) (word (Word_ext f B_ant))) *)
(* Goal: inmonoid (union (map f X) (map f V1)) (Word_ext f B_ant) *)
(* Goal: @ex Elt (fun x_ant : Elt => and (dans x_ant R1) (@eq Elt x (fonc x_ant))) *)
	rewrite x_egal; unfold fonc in |- *; unfold fet in |- *.
	rewrite x_ant_egal; unfold first in |- *; unfold second in |- *;
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
  unfold word_inv in |- *; simpl in |- *.
(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	trivial.
	replace (union (map f X) (map f V1)) with (map f (union X V1));
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
  auto.

(* Goal: Id (union X (add a V1')) f *)
apply dans_map; assumption. (*1*)
Qed.


Lemma image_isGram :
 isGram X V1 R1 S1 ->
 Mots Xim -> inter Xim Vim empty -> isGram Xim Vim Rim Sim.

(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
unfold Sim, Rim, Gim3, Vim, Gim2, Xim, Gim, imageGram in |- *; simpl in |- *.
(* Goal: forall (_ : isGram X V1 R1 S1) (_ : Mots (map f X)) (_ : inter (map f X) (map f V1) empty), isGram (map f X) (map f V1) (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R1) (f S1) *)
prolog [ isGram4 image_Regles isGram3 dans_map_inv isGram5 ] 7.

(*Intro is_Gram; Intro Mots ; Intro intersec .
Apply isGram5. 
 Assumption.
 Assumption.
 Apply dans_map_inv ; Apply isGram3 with X R1 ; Assumption.
 Apply image_Regles; Apply isGram4 with S1; Assumption.*)

Qed.


Lemma Id_image_X : Id (union X V1) f -> Xim = X :>Ensf.

(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
unfold Xim, Gim, imageGram in |- *; simpl in |- *.
(* Goal: forall _ : Id (union X V1) f, @eq Ensf (map f X) X *)
elim X.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
auto.
(* Clear X. *)
(* Goal: forall (e : Elt) (e0 : Ensf) (_ : forall _ : Id (union e0 V1) f, @eq Ensf (map f e0) e0) (_ : Id (union (add e e0) V1) f), @eq Ensf (map f (add e e0)) (add e e0) *)
intros a X' Hyp Id_a_X_V1_f.
(* Goal: @eq Ensf (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) (add a R)) (add a R) *)
unfold map in |- *.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
simpl in |- *.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
apply add_add.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	auto.

(* Goal: (fun w w0 : Word => Rstar Word (Derive Rim) (wef w) (wef w0)) u v *)
	apply Hyp.
(* Goal: Id (union X' V1) f *)
	apply Id_inclus with (union (add a X') V1).

(* Goal: inclus (union X V1') (union X (add a V1')) *)
(* Goal: Id (union X (add a V1')) f *)
		red in |- *; intros x dans_x_union_X_V1.
(* Goal: dans x (union (add a X') V1) *)
(* Goal: Id (union (add a X') V1) f *)
		cut (dans x X' \/ dans x V1). 
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	        intros [HX| HV1]; auto.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		auto.

(* Goal: Id (union X (add a V1')) f *)
		assumption.
Qed.

Lemma Id_image_V : Id (union X V1) f -> Vim = V1 :>Ensf.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
unfold Vim, Gim2, Gim, imageGram; simpl in |- *.
(* Goal: forall _ : Id (union X V1) f, @eq Ensf (map f V1) V1 *)
generalize V1; clearbody C Gim; clear V1.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
simple induction V1; auto.
(* Goal: forall (e : Elt) (e0 : Ensf) (_ : forall _ : Id (union X e0) f, @eq Ensf (map f e0) e0) (_ : Id (union X (add e e0)) f), @eq Ensf (map f (add e e0)) (add e e0) *)
intros a V1' Hyp Id_X_a_V1_f.
(* Goal: @eq Ensf (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) (add a R)) (add a R) *)
unfold map in |- *.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
simpl in |- *.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
apply add_add.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	auto.

(* Goal: (fun w w0 : Word => Rstar Word (Derive Rim) (wef w) (wef w0)) u v *)
	apply Hyp.
(* Goal: Id (union X V1') f *)
	apply Id_inclus with (union X (add a V1')).
(* Goal: inclus (union X V1') (union X (add a V1')) *)
(* Goal: Id (union X (add a V1')) f *)
		red in |- *; intros x dans_x_union_X_V1.
(* Goal: dans x (union X (add a V1')) *)
(* Goal: Id (union X (add a V1')) f *)
		cut (dans x X \/ dans x V1'). 
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		intros [HX| HV1]; auto.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		auto.
					
(* Goal: Id (union X (add a V1')) f *)
		assumption.
Qed.

Lemma Id_image_R : Id (union X V1) f -> isGram X V1 R1 S1 -> Rim = R1 :>Ensf.
(* Goal: forall (_ : Id (union X V1) f) (_ : isGram X V1 R1 S1), @eq Ensf Rim R1 *)
intros Id_X_V1_f.

(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
unfold Rim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *.
(* Goal: forall _ : isGram X V1 R1 S1, @eq Ensf (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R1) R1 *)
elim R1.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
auto.
(* Goal: forall (e : Elt) (e0 : Ensf) (_ : forall _ : isGram X V1 e0 S1, @eq Ensf (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) e0) e0) (_ : isGram X V1 (add e e0) S1), @eq Ensf (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) (add e e0)) (add e e0) *)
intros a R Hyp isGram_X_V1_R1_S1.
(* Goal: @eq Ensf (map (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) (add a R)) (add a R) *)
unfold map in |- *.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
simpl in |- *.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
apply add_add.

(* Goal: @eq Elt (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) a *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	cut (Regles X V1 (add a R)).
(* Goal: forall _ : Regles X V1 (add a R), @eq Elt (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) a *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	unfold Regles in |- *.
(* Goal: forall _ : forall (x : Elt) (_ : dans x (add a R)), @ex2 Elt (fun A : Elt => dans A V1) (fun A : Elt => @ex2 Word (fun B : Word => @eq Elt x (couple A (word B))) (fun B : Word => inmonoid (union X V1) B)), @eq Elt (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) a *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	intro R_a_R.
(* Goal: @eq Elt (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) a *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	elim (R_a_R a).
(* Goal: forall (x : Elt) (_ : dans x V1) (_ : @ex2 Word (fun B : Word => @eq Elt a (couple x (word B))) (fun B : Word => inmonoid (union X V1) B)), @eq Elt (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) a *)
(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	intros x dans_x_V1 temp; elim temp; clear temp.
(* Goal: forall (x0 : Word) (_ : @eq Elt a (couple x (word x0))) (_ : inmonoid (union X V1) x0), @eq Elt (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) a *)
(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	intros B egal_a inmonoid_B.

(* Goal: @eq Elt (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) a *)
(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	rewrite egal_a.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
	apply couple_couple; unfold first, second, word_inv in |- *; simpl in |- *.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		auto.

(* Goal: @eq Elt (word (Word_ext f B)) (word B) *)
(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
		apply word_word.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		cut (Id_words (union X V1) (Word_ext f)); auto.
		

(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	trivial.

(* Goal: dans a (add a R) *)
(* Goal: Regles X V1 (add a R) *)
(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	apply isGram4 with S1; trivial.

(* Goal: @eq Ensf ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R) R *)
	prolog [ isGram_inclus3 ] 3.
	(*Apply Hyp.
	Apply isGram_inclus3 with a; Assumption.*)
Qed.

Lemma Id_image_S : Id (union X V1) f -> isGram X V1 R1 S1 -> Sim = S1 :>Elt.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
unfold Sim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *.
(* Goal: forall (_ : Id (union X V1) f) (_ : isGram X V1 R1 S1), @eq Elt (f S1) S1 *)
prolog [ isGram3 union_d ] 6.
(*Intros Id_union_X_V1_f isGram_X_V1_R1_S1.
Apply Id_union_X_V1_f.
Apply union_d.
Apply isGram3 with X R1; Assumption.*)
Qed.

Lemma Gim_egal : Gim = (Xim, (Vim, (Rim, Sim))).
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) Gim (@pair Ensf (prod Ensf (prod Ensf Elt)) Xim (@pair Ensf (prod Ensf Elt) Vim (@pair Ensf Elt Rim Sim))) *)
unfold Sim, Rim, Gim3, Vim, Gim2, Xim in |- *.
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
apply refl_equal.
Qed.



Lemma Id_image_G :
 Id (union X V1) f -> isGram X V1 R1 S1 -> Gim = (X, (V1, (R1, S1))).
(* Goal: forall (_ : Id (union X V1) f) (_ : isGram X V1 R1 S1), @eq (prod Ensf (prod Ensf (prod Ensf Elt))) Gim (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
intros Id_u_X_V1_f isG_X_V1_R1_S1.
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) Gim (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
rewrite Gim_egal.

(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) (@pair Ensf (prod Ensf (prod Ensf Elt)) Xim (@pair Ensf (prod Ensf Elt) Vim (@pair Ensf Elt Rim Sim))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
rewrite (Id_image_S Id_u_X_V1_f isG_X_V1_R1_S1).
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) (@pair Ensf (prod Ensf (prod Ensf Elt)) Xim (@pair Ensf (prod Ensf Elt) Vim (@pair Ensf Elt Rim S1))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
rewrite (Id_image_R Id_u_X_V1_f isG_X_V1_R1_S1).
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) (@pair Ensf (prod Ensf (prod Ensf Elt)) Xim (@pair Ensf (prod Ensf Elt) Vim (@pair Ensf Elt R1 S1))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
rewrite (Id_image_V Id_u_X_V1_f).
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) (@pair Ensf (prod Ensf (prod Ensf Elt)) Xim (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
rewrite (Id_image_X Id_u_X_V1_f).
(* Goal: @eq (prod Ensf (prod Ensf (prod Ensf Elt))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) (@pair Ensf (prod Ensf (prod Ensf Elt)) X (@pair Ensf (prod Ensf Elt) V1 (@pair Ensf Elt R1 S1))) *)
apply refl_equal.
Qed.

Lemma Derive_image :
 forall u v : Word, Derive R1 u v -> Derive Rim (wef u) (wef v).

(* Goal: forall (u v : Word) (_ : Derive R1 u v), Derive Rim (wef u) (wef v) *)
intros u v H.
(* Goal: Derive Rim (wef u) (wef v) *)
elim H; clear H u v.
(* Goal: forall (u v : Word) (A : Elt) (_ : dans (couple A (word u)) R1), Derive Rim (wef (cons A v)) (wef (Append u v)) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R1 u v) (_ : Derive Rim (wef u) (wef v)), Derive Rim (wef (cons x u)) (wef (cons x v)) *)
	intros u v A dans_A.
(* Goal: Derive Rim (wef (cons A v)) (wef (Append u v)) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R1 u v) (_ : Derive Rim (wef u) (wef v)), Derive Rim (wef (cons x u)) (wef (cons x v)) *)
	replace (wef (cons A v)) with (cons (f A) (wef v)).
(* Goal: Derive Rim (cons (f A) (wef v)) (wef (Append u v)) *)
(* Goal: @eq Word (cons (f A) (wef v)) (wef (cons A v)) *)
(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R1 u v) (_ : Derive Rim (wef u) (wef v)), Derive Rim (wef (cons x u)) (wef (cons x v)) *)
	replace (wef (Append u v)) with (Append (wef u) (wef v)).
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	auto.

(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	apply sym_equal; unfold wef in |- *; apply wef_append; auto.

(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	auto.

(* Goal: forall (u v : Word) (x : Elt) (_ : Derive R1 u v) (_ : Derive Rim (wef u) (wef v)), Derive Rim (wef (cons x u)) (wef (cons x v)) *)
	intros.
(* Goal: Derive Rim (wef (cons x u)) (wef (cons x v)) *)
	replace (wef (cons x u)) with (cons (f x) (wef u)).
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	 replace (wef (cons x v)) with (cons (f x) (wef v)); auto.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	 auto.
Qed.

Hint Resolve Derive_image.

Lemma Derivestar_image :
 forall u v : Word, Derivestar R1 u v -> Derivestar Rim (wef u) (wef v).
(* Goal: forall (u v : Word) (_ : Derivestar R1 u v), Derivestar Rim (wef u) (wef v) *)
unfold Derivestar in |- *.
(* Goal: forall (u v : Word) (_ : Rstar Word (Derive R1) u v), Rstar Word (Derive Rim) (wef u) (wef v) *)
intros u v Hyp.
(* Goal: Rstar Word (Derive Rim) (wef u) (wef v) *)
unfold Derivestar, Rstar in Hyp.
(* Goal: Rstar Word (Derive Rim) (wef u) (wef v) *)
pattern u, v in |- *.
(* Goal: (fun w w0 : Word => Rstar Word (Derive Rim) (wef w) (wef w0)) u v *)
apply Hyp.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	auto. (*Intros; Apply Rstar_reflexive. *)
(* Goal: forall (u v w : Word) (_ : Derive R1 u v) (_ : Rstar Word (Derive Rim) (wef v) (wef w)), Rstar Word (Derive Rim) (wef u) (wef w) *)
	intros a b c DeriveR1 Rst.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	apply Rstar_R with (y := wef b); auto.
Qed.

Hint Resolve Derivestar_image.


Lemma Reconnait_imageGram :
 forall w : Word, LG X V1 R1 S1 w -> LG Xim Vim Rim Sim (wef w).
 
(* Goal: forall (w : Word) (_ : LG X V1 R1 S1 w), LG Xim Vim Rim Sim (wef w) *)
intro w.
(* Goal: forall _ : LG X V1 R1 S1 w, LG Xim Vim Rim Sim (wef w) *)
unfold LG in |- *.
(* Goal: forall _ : and (Derivestar R1 (cons S1 nil) w) (inmonoid X w), and (Derivestar Rim (cons Sim nil) (wef w)) (inmonoid Xim (wef w)) *)
intro temp; split; elim temp; clear temp; intros Der inmo.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
	unfold Sim, Gim3, Gim2, Gim, imageGram in |- *; simpl in |- *.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
	replace (cons (f S1) nil) with (wef (cons S1 nil)); auto.

(* Goal: inmonoid Xim (wef w) *)
	elim inmo.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		auto.
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		intros wo el.
(* Goal: @eq Ensf (add (couple (f (first a)) (word (Word_ext f (word_inv (second a))))) ((fix map (f : forall _ : Elt, Elt) (e : Ensf) {struct e} : Ensf := match e with | empty => empty | add y e0 => add (f y) (map f e0) end) (fun P : Elt => couple (f (first P)) (word (Word_ext f (word_inv (second P))))) R)) (add a R) *)
		unfold Xim, Gim, imageGram in |- *; simpl in |- *.
(* Goal: inmonoid Xim (wef nil) *)
(* Goal: forall (w : Word) (e : Elt) (_ : inmonoid X w) (_ : inmonoid Xim (wef w)) (_ : dans e X), inmonoid Xim (wef (cons e w)) *)
		replace (wef (cons el wo)) with (cons (f el) (wef wo)); auto.
Qed.


End resultats.

Hint Resolve dans_Rim.
Hint Resolve Derive_image.
Hint Resolve Derivestar_image.
Hint Resolve Reconnait_imageGram.
