(* 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                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 gram5.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 Rat.
Require Import need.
Require Import fonctions.
Require Import Relations.
Require Import gram.
Require Import gram2.
Require Import gram3.
Require Import gram4.

Section gram5.

Variable X : Ensf.

Variable V1 R1 : Ensf.
Variable S1 : Elt.

Variable V2 R2 : Ensf.
Variable S2 : Elt.

Let S' := zero.

Let G1 := imageGram (injproducg V1) X V1 R1 S1.
Let G2 := imageGram (injproducd V2) X V2 R2 S2.
Let X1' := fst G1.
Let GG1 := snd G1.
Let V1' := fst GG1.
Let GGG1 := snd GG1.
Let R1' := fst GGG1.
Let S1' := snd GGG1.

Let X2' := fst G2.
Let GG2 := snd G2.
Let V2' := fst GG2.
Let GGG2 := snd GG2.
Let R2' := fst GGG2.
Let S2' := snd GGG2.

Let Gim := Gunion_disj_p V1' R1' S1' V2' R2' S2' S'.
Let Vu := fst Gim.
Let C' := snd Gim.
Let Ru := fst C'.
Let Su := snd C'.

Hypothesis Grammaire1 : isGram X V1 R1 S1.
Hypothesis Grammaire2 : isGram X V2 R2 S2.
Hint Resolve Grammaire1.
Hint Resolve Grammaire2.


Lemma Mots_X : Mots X.
(* Goal: Mots X *)
apply isGram1 with V1 R1 S1.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve Mots_X.

Lemma int_X_V1_empty : inter X V1 empty.
(* Goal: inter X V1 empty *)
apply isGram2 with R1 S1.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve int_X_V1_empty.

Lemma int_X_V2_empty : inter X V2 empty.
(* Goal: inter X V2 empty *)
apply isGram2 with R2 S2.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve int_X_V2_empty.



Definition Gunion_disj := Gim.


Let Vim := fst Gunion_disj.
Let GGim := snd Gunion_disj.
Let Rim := fst GGim.
Let Sim := snd GGim.


Lemma Id_injproducg1 : forall x : Elt, dans x X -> injproducg V1 x = x :>Elt.
(* Goal: forall (x : Elt) (_ : dans x X), @eq Elt (injproducg V1 x) x *)
unfold Id, injproducg in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
simpl in |- *.
(* Goal: forall (x : Elt) (_ : dans x X), @eq Elt (extension V2 injdroite x) x *)
intros x dans_x_X.
(* Goal: @eq Elt (extension V2 injdroite x) x *)
apply extension_out.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply inter_dans with X; auto.
Qed.
Hint Resolve Id_injproducg1.


Lemma Id_injproducd2 : forall x : Elt, dans x X -> injproducd V2 x = x :>Elt.
(* Goal: forall (x : Elt) (_ : dans x X), @eq Elt (injproducd V2 x) x *)
unfold Id, injproducd in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
simpl in |- *.
(* Goal: forall (x : Elt) (_ : dans x X), @eq Elt (extension V2 injdroite x) x *)
intros x dans_x_X.
(* Goal: @eq Elt (extension V2 injdroite x) x *)
apply extension_out.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply inter_dans with X; auto.
Qed.
Hint Resolve Id_injproducd2.

Lemma N_dans_S_X : ~ dans S' X.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: forall _ : dans S' X, False *)
intro dans_S_X.
(* Goal: False *)
elimtype (exists w : Word, word w = S').
(* Goal: forall (x : Word) (_ : @eq Elt (word x) S'), False *)
(* Goal: @ex Word (fun w : Word => @eq Elt (word w) S') *)
	intro x.
(* Goal: forall _ : @eq Elt (word x) S', False *)
(* Goal: @ex Word (fun w : Word => @eq Elt (word w) S') *)
	change (word x <> natural 0) in |- *.
(* Goal: not (@eq Elt (word x0) (couple x un)) *)
(* Goal: @eq Elt (word x0) (couple x un) *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
	discriminate.
(* Goal: @ex Word (fun w : Word => @eq Elt (word w) S') *)
apply Mots_X; assumption.
Qed.
Hint Resolve N_dans_S_X.

Lemma injproducg_V1 :
 forall x : Elt, dans x V1 -> injproducg V1 x = injgauche x.
(* Goal: forall (x : Elt) (_ : dans x V1), @eq Elt (injproducg V1 x) (injgauche x) *)
intros x dans_x_V1.
(* Goal: @eq Elt (injproducg V1 x) (injgauche x) *)
unfold injproducg, extension in |- *.
(* Goal: @eq Elt (let (y, _) := extension_spec V1 injgauche x in y) (injgauche x) *)
elim (extension_spec V1 injgauche x).
(* Goal: forall (x0 : Elt) (_ : or (and (dans x V2) (@eq Elt x0 (injdroite x))) (and (not (dans x V2)) (@eq Elt x0 x))), @eq Elt x0 (injdroite x) *)
intros x0 temp; elim temp; clear temp; intro temp; elim temp; clear temp.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	auto.
(* Goal: forall _ : @eq Elt (couple x un) (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
	intros.
(* Goal: @eq Elt x0 (injgauche x) *)
	absurd (dans x V1); assumption.
Qed.
Hint Resolve injproducg_V1.


Lemma map_injproducg_V1 : map (injproducg V1) V1 = map injgauche V1 :>Ensf.
(* Goal: @eq Ensf (map (injproducd V2) V2) (map injdroite V2) *)
apply map_egal.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve map_injproducg_V1.

Lemma injproducd_V2 :
 forall x : Elt, dans x V2 -> injproducd V2 x = injdroite x.
(* Goal: forall (x : Elt) (_ : dans x V2), @eq Elt (injproducd V2 x) (injdroite x) *)
intros x dans_x_V2.
(* Goal: @eq Elt (injproducd V2 x) (injdroite x) *)
unfold injproducd, extension in |- *.
(* Goal: @eq Elt (let (y, _) := extension_spec V2 injdroite x in y) (injdroite x) *)
elim (extension_spec V2 injdroite x).
(* Goal: forall (x0 : Elt) (_ : or (and (dans x V2) (@eq Elt x0 (injdroite x))) (and (not (dans x V2)) (@eq Elt x0 x))), @eq Elt x0 (injdroite x) *)
intros x0 temp; elim temp; clear temp; intro temp; elim temp; clear temp.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	auto.
(* Goal: forall _ : @eq Elt (couple x un) (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
	intros.
(* Goal: @eq Elt x0 (injdroite x) *)
	absurd (dans x V2); assumption.
Qed.
Hint Resolve injproducd_V2.


Lemma map_injproducd_V2 : map (injproducd V2) V2 = map injdroite V2 :>Ensf.
(* Goal: @eq Ensf (map (injproducd V2) V2) (map injdroite V2) *)
apply map_egal.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve map_injproducd_V2.



Lemma N_dans_S_V1' : ~ dans S' V1'.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: forall _ : dans S' V1', False *)
replace V1' with (map injgauche V1).
(* Goal: forall _ : @eq Elt (couple x un) (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros.
(* Goal: False *)
(* Goal: @eq Ensf (map injgauche V1) V1' *)
elimtype (exists y : Elt, dans y V1 /\ S' = (fun e : Elt => couple e zero) y).
(* Goal: forall (x : Elt) (_ : and (dans x V2) (@eq Elt S' (couple x un))), False *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt S' (couple y un))) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
intros x temp; elim temp; clear temp.
(* Goal: forall (_ : dans x V1) (_ : @eq Elt S' (couple x zero)), False *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt S' (couple y zero))) *)
(* Goal: @eq Ensf (map injgauche V1) V1' *)
intros dans_x_V1 S_egal.
(* Goal: False *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt S' (couple y zero))) *)
(* Goal: @eq Ensf (map injgauche V1) V1' *)
absurd (S' = couple x zero).
(* Goal: not (@eq Elt S' (couple x un)) *)
(* Goal: @eq Elt S' (couple x un) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt S' (couple y un))) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
unfold S', zero in |- *.
(* Goal: not (@eq Elt (word x0) (couple x un)) *)
(* Goal: @eq Elt (word x0) (couple x un) *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
discriminate.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt S' (couple y zero))) *)
(* Goal: @eq Ensf (map injgauche V1) V1' *)
apply (dans_map (fun e : Elt => couple e zero)).
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
assumption.
(* Goal: @eq Ensf (map injgauche V1) V1' *)
unfold V1' in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
simpl in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve N_dans_S_V1'.


Lemma N_dans_S_V2' : ~ dans S' V2'.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: forall _ : dans S' V2', False *)
replace V2' with (map injdroite V2).
(* Goal: forall _ : @eq Elt (injdroite x) (injdroite y), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
unfold injdroite in |- *.
(* Goal: forall _ : @eq Elt (couple x un) (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros.
(* Goal: False *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
elimtype (exists y : Elt, dans y V2 /\ S' = (fun e : Elt => couple e un) y).
(* Goal: forall (x : Elt) (_ : and (dans x V2) (@eq Elt S' (couple x un))), False *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt S' (couple y un))) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
intros x temp; elim temp; clear temp.
(* Goal: forall (_ : dans x V2) (_ : @eq Elt S' (couple x un)), False *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt S' (couple y un))) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
intros dans_x_V2 S_egal.
(* Goal: False *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt S' (couple y un))) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
absurd (S' = couple x un).
(* Goal: not (@eq Elt S' (couple x un)) *)
(* Goal: @eq Elt S' (couple x un) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt S' (couple y un))) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
unfold S', zero in |- *.
(* Goal: not (@eq Elt (word x0) (couple x un)) *)
(* Goal: @eq Elt (word x0) (couple x un) *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
discriminate.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt S' (couple y un))) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply (dans_map (fun e : Elt => couple e un)).
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
assumption.
(* Goal: @eq Ensf (map injdroite V2) V2' *)
unfold V2' in |- *.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
simpl in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.

Hint Resolve N_dans_S_V2'.

Lemma is_mono_u_X_V1_injproducg_V1 : is_mono (union X V1) (injproducg V1).
(* Goal: is_mono (union X V2) (injproducd V2) *)
unfold is_mono in |- *.
(* Goal: forall (x y : Elt) (_ : dans x (union X V2)) (_ : dans y (union X V2)) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
intros x y dans_x_u dans_y_u.
(* Goal: forall _ : @eq Elt (injproducg V1 x) (injproducg V1 y), @eq Elt x y *)
elimtype (dans x X \/ dans x V1).
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
intro dans_x.
(* Goal: forall _ : @eq Elt (injproducg V1 x) (injproducg V1 y), @eq Elt x y *)
(* Goal: forall (_ : dans x V1) (_ : @eq Elt (injproducg V1 x) (injproducg V1 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V1) *)
replace (injproducg V1 x) with x.

(* Goal: forall _ : @eq Elt (injgauche x) (injproducg V1 y), @eq Elt x y *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
elimtype (dans y X \/ dans y V1).
(* Goal: forall (_ : dans y X) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros dans_y.
(* Goal: forall _ : @eq Elt (injgauche x) (injproducg V1 y), @eq Elt x y *)
(* Goal: forall (_ : dans y V1) (_ : @eq Elt (injgauche x) (injproducg V1 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
replace (injproducg V1 y) with y.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: forall (_ : dans y X) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros dans_y.
(* Goal: forall _ : @eq Elt (injgauche x) (injproducg V1 y), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
replace (injproducg V1 y) with (injgauche y).
(* Goal: forall _ : @eq Elt (injgauche x) (injgauche y), @eq Elt x y *)
(* Goal: @eq Elt (injgauche y) (injproducg V1 y) *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
unfold injgauche in |- *.
(* Goal: forall _ : @eq Elt x (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt x (injproducd V2 x) *)
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
elim (Mots_X x dans_x).
(* Goal: forall (x0 : Word) (_ : @eq Elt (word x0) x) (_ : @eq Elt x (couple y un)), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt x (injproducd V2 x) *)
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
intros x0 egal_x egal2_x.
(* Goal: @eq Elt x y *)
(* Goal: @eq Elt (injgauche y) (injproducg V1 y) *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt x (injproducg V1 x) *)
(* Goal: forall (_ : dans x V1) (_ : @eq Elt (injproducg V1 x) (injproducg V1 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V1) *)
absurd (word x0 = couple y zero).
(* Goal: not (@eq Elt (word x0) (couple x un)) *)
(* Goal: @eq Elt (word x0) (couple x un) *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
	discriminate.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
	rewrite egal_x; assumption.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
intro dans_x.
(* Goal: forall _ : @eq Elt (injproducg V1 x) (injproducg V1 y), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V1) *)
replace (injproducg V1 x) with (injgauche x).
(* Goal: forall _ : @eq Elt (injgauche x) (injproducg V1 y), @eq Elt x y *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
elimtype (dans y X \/ dans y V1).
(* Goal: forall (_ : dans y X) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros dans_y.
(* Goal: forall _ : @eq Elt (injgauche x) (injproducg V1 y), @eq Elt x y *)
(* Goal: forall (_ : dans y V1) (_ : @eq Elt (injgauche x) (injproducg V1 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
replace (injproducg V1 y) with y.
(* Goal: forall _ : @eq Elt (injgauche x) (injgauche y), @eq Elt x y *)
(* Goal: @eq Elt (injgauche y) (injproducg V1 y) *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
unfold injgauche in |- *.
(* Goal: forall _ : @eq Elt (couple x un) y, @eq Elt x y *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
elim (Mots_X y dans_y).
(* Goal: forall (x0 : Word) (_ : @eq Elt (word x0) y) (_ : @eq Elt (couple x un) y), @eq Elt x y *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros x0 egal_y egal2_y.
(* Goal: @eq Elt x y *)
(* Goal: @eq Elt y (injproducg V1 y) *)
(* Goal: forall (_ : dans y V1) (_ : @eq Elt (injgauche x) (injproducg V1 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
absurd (word x0 = couple x zero).
(* Goal: not (@eq Elt (word x0) (couple x un)) *)
(* Goal: @eq Elt (word x0) (couple x un) *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
	discriminate.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
	rewrite egal2_y; assumption.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: forall _ : @eq Elt (natural O) (natural (S O)), False *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
intro.
(* Goal: forall _ : @eq Elt (injgauche x) (injproducg V1 y), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
replace (injproducg V1 y) with (injgauche y).
(* Goal: forall _ : @eq Elt (injgauche x) (injgauche y), @eq Elt x y *)
(* Goal: @eq Elt (injgauche y) (injproducg V1 y) *)
(* Goal: or (dans y X) (dans y V1) *)
(* Goal: @eq Elt (injgauche x) (injproducg V1 x) *)
(* Goal: or (dans x X) (dans x V1) *)
unfold injgauche in |- *.
(* Goal: forall _ : @eq Elt (couple x un) (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply couple_couple_inv1 with zero zero; assumption.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve is_mono_u_X_V1_injproducg_V1.


Lemma is_mono_u_X_V2_injproducd_V2 : is_mono (union X V2) (injproducd V2).
(* Goal: is_mono (union X V2) (injproducd V2) *)
unfold is_mono in |- *.
(* Goal: forall (x y : Elt) (_ : dans x (union X V2)) (_ : dans y (union X V2)) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
intros x y dans_x_u dans_y_u.
(* Goal: forall _ : @eq Elt (injproducd V2 x) (injproducd V2 y), @eq Elt x y *)
elimtype (dans x X \/ dans x V2).
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
intro dans_x.
(* Goal: forall _ : @eq Elt (injproducd V2 x) (injproducd V2 y), @eq Elt x y *)
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
replace (injproducd V2 x) with x.

(* Goal: forall _ : @eq Elt (injdroite x) (injproducd V2 y), @eq Elt x y *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
elimtype (dans y X \/ dans y V2).
(* Goal: forall (_ : dans y X) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros dans_y.
(* Goal: forall _ : @eq Elt (injdroite x) (injproducd V2 y), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
replace (injproducd V2 y) with y.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: forall (_ : dans y X) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros dans_y.
(* Goal: forall _ : @eq Elt (injdroite x) (injproducd V2 y), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
replace (injproducd V2 y) with (injdroite y).
(* Goal: forall _ : @eq Elt (injdroite x) (injdroite y), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
unfold injdroite in |- *.
(* Goal: forall _ : @eq Elt x (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt x (injproducd V2 x) *)
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
elim (Mots_X x dans_x).
(* Goal: forall (x0 : Word) (_ : @eq Elt (word x0) x) (_ : @eq Elt x (couple y un)), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt x (injproducd V2 x) *)
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
intros x0 egal_x egal2_x.
(* Goal: @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt x (injproducd V2 x) *)
(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
absurd (word x0 = couple y un).
(* Goal: not (@eq Elt (word x0) (couple x un)) *)
(* Goal: @eq Elt (word x0) (couple x un) *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
	discriminate.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
	rewrite egal_x; assumption.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: forall (_ : dans x V2) (_ : @eq Elt (injproducd V2 x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
intro dans_x.
(* Goal: forall _ : @eq Elt (injproducd V2 x) (injproducd V2 y), @eq Elt x y *)
(* Goal: or (dans x X) (dans x V2) *)
replace (injproducd V2 x) with (injdroite x).
(* Goal: forall _ : @eq Elt (injdroite x) (injproducd V2 y), @eq Elt x y *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
elimtype (dans y X \/ dans y V2).
(* Goal: forall (_ : dans y X) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros dans_y.
(* Goal: forall _ : @eq Elt (injdroite x) (injproducd V2 y), @eq Elt x y *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
replace (injproducd V2 y) with y.
(* Goal: forall _ : @eq Elt (injdroite x) (injdroite y), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
unfold injdroite in |- *.
(* Goal: forall _ : @eq Elt (couple x un) y, @eq Elt x y *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
elim (Mots_X y dans_y).
(* Goal: forall (x0 : Word) (_ : @eq Elt (word x0) y) (_ : @eq Elt (couple x un) y), @eq Elt x y *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros x0 egal_y egal2_y.
(* Goal: @eq Elt x y *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
absurd (word x0 = couple x un).
(* Goal: not (@eq Elt (word x0) (couple x un)) *)
(* Goal: @eq Elt (word x0) (couple x un) *)
(* Goal: @eq Elt y (injproducd V2 y) *)
(* Goal: forall (_ : dans y V2) (_ : @eq Elt (injdroite x) (injproducd V2 y)), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
	discriminate.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
	rewrite egal2_y; assumption.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: forall _ : @eq Elt (natural O) (natural (S O)), False *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
intro.
(* Goal: forall _ : @eq Elt (injdroite x) (injproducd V2 y), @eq Elt x y *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
replace (injproducd V2 y) with (injdroite y).
(* Goal: forall _ : @eq Elt (injdroite x) (injdroite y), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
unfold injdroite in |- *.
(* Goal: forall _ : @eq Elt (couple x un) (couple y un), @eq Elt x y *)
(* Goal: @eq Elt (injdroite y) (injproducd V2 y) *)
(* Goal: or (dans y X) (dans y V2) *)
(* Goal: @eq Elt (injdroite x) (injproducd V2 x) *)
(* Goal: or (dans x X) (dans x V2) *)
intros.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply couple_couple_inv1 with un un; assumption.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
apply sym_equal; auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve is_mono_u_X_V2_injproducd_V2.



Lemma egal_LG_1_1' : l_egal (LG X V1 R1 S1) (LG X V1' R1' S1').
(* Goal: l_egal (LG X V2 R2 S2) (LG X V2' R2' S2') *)
pattern X at 2 in |- *.
(* Goal: (fun e : Ensf => l_egal (LG X V1 R1 S1) (LG e V1' R1' S1')) X *)
replace X with X1'.
(* Goal: isGram X1' V1' R1' S1' *)
unfold X1', V1', R1', S1', GGG1, GG1, G1 in |- *.
(* Goal: l_egal (LG X V2 R2 S2) (LG (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))) (@fst Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)))) (@snd Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))))) *)
(* Goal: @eq Ensf X2' X *)
apply egal_LG.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
red in |- *; auto.

(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
unfold X1' in |- *; simpl in |- *.
(* Goal: @eq Ensf (map (injproducd V2) X) X *)
apply map_Id.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

Qed.
Hint Resolve egal_LG_1_1'.


Lemma egal_LG_2_2' : l_egal (LG X V2 R2 S2) (LG X V2' R2' S2').
(* Goal: l_egal (LG X V2 R2 S2) (LG X V2' R2' S2') *)
pattern X at 2 in |- *.
(* Goal: (fun e : Ensf => l_egal (LG X V2 R2 S2) (LG e V2' R2' S2')) X *)
replace X with X2'.

(* Goal: isGram X2' V2' R2' S2' *)
unfold X2', V2', R2', S2', GGG2, GG2, G2 in |- *.
(* Goal: l_egal (LG X V2 R2 S2) (LG (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))) (@fst Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)))) (@snd Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))))) *)
(* Goal: @eq Ensf X2' X *)
apply egal_LG.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
red in |- *; auto.

(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
unfold X2' in |- *; simpl in |- *.
(* Goal: @eq Ensf (map (injproducd V2) X) X *)
apply map_Id.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

Qed.
Hint Resolve egal_LG_2_2'.



Lemma egal_X_X1' : X1' = X :>Ensf.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
unfold X1' in |- *. simpl in |- *.
(* Goal: @eq Ensf (map (injproducd V2) X) X *)
apply map_Id.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.

Lemma egal_X_X2' : X2' = X :>Ensf.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
unfold X2' in |- *. simpl in |- *.
(* Goal: @eq Ensf (map (injproducd V2) X) X *)
apply map_Id.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.


Lemma Grammaire1' : isGram X V1' R1' S1'.
(* Goal: isGram X V1' R1' S1' *)
rewrite <- egal_X_X1'.
(* Goal: isGram X1' V1' R1' S1' *)
unfold X1', V1', R1', S1', GGG1, GG1, G1 in |- *.
(* Goal: isGram (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))) (@fst Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)))) (@snd Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)))) *)
apply image_isGram.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	auto.

(* Goal: Mots (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducg V1) X V1 R1 S1)) *)
(* Goal: inter (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducg V1) X V1 R1 S1)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducg V1) X V1 R1 S1))) empty *)
	change (Mots X1') in |- *.
(* Goal: Mots X1' *)
(* Goal: inter (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducg V1) X V1 R1 S1)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducg V1) X V1 R1 S1))) empty *)
	rewrite egal_X_X1'.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	apply inter_Xim_Vim_empty; auto.

Qed.
Hint Resolve Grammaire1'.


Lemma Grammaire2' : isGram X V2' R2' S2'.
(* Goal: isGram X V2' R2' S2' *)
rewrite <- egal_X_X2'.
(* Goal: isGram X2' V2' R2' S2' *)
unfold X2', V2', R2', S2', GGG2, GG2, G2 in |- *.
(* Goal: isGram (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))) (@fst Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)))) (@snd Ensf Elt (@snd Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)))) *)
apply image_isGram.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	auto.

(* Goal: Mots (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)) *)
(* Goal: inter (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))) empty *)
	change (Mots X2') in |- *.
(* Goal: Mots X2' *)
(* Goal: inter (@fst Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2)) (@fst Ensf (prod Ensf Elt) (@snd Ensf (prod Ensf (prod Ensf Elt)) (imageGram (injproducd V2) X V2 R2 S2))) empty *)
	rewrite egal_X_X2'.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	auto.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
	apply inter_Xim_Vim_empty; auto.

Qed.
Hint Resolve Grammaire2'.

Lemma inter_V1'_V2'_empty : inter V1' V2' empty.
(* Goal: @eq Ensf (@fst Ensf (prod Ensf (prod Ensf Elt)) G2) X *)
unfold V1', V2' in |- *; simpl in |- *.
(* Goal: inter (map (injproducg V1) V1) (map (injproducd V2) V2) empty *)
unfold inter in |- *.
(* Goal: and (inclus empty (map (injproducg V1) V1)) (and (inclus empty (map (injproducd V2) V2)) (forall (x : Elt) (_ : dans x (map (injproducg V1) V1)) (_ : dans x (map (injproducd V2) V2)), dans x empty)) *)
split; [ auto | split ].
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

(* Goal: forall (x : Elt) (_ : dans x (map (injproducg V1) V1)) (_ : dans x (map (injproducd V2) V2)), dans x empty *)
replace (map (injproducg V1) V1) with (map injgauche V1).
(* Goal: forall (x : Elt) (_ : dans x (map injgauche V1)) (_ : dans x (map (injproducd V2) V2)), dans x empty *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
replace (map (injproducd V2) V2) with (map injdroite V2).
(* Goal: forall (x : Elt) (_ : dans x (map injgauche V1)) (_ : dans x (map injdroite V2)), dans x empty *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
intros x dans_map_1 dans_map_2.
(* Goal: dans x empty *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
elimtype (exists y : Elt, dans y V1 /\ x = injgauche y).
(* Goal: forall (x0 : Elt) (_ : and (dans x0 V1) (@eq Elt x (injgauche x0))), dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
elimtype (exists y : Elt, dans y V2 /\ x = injdroite y).
(* Goal: forall (x0 : Elt) (_ : and (dans x0 V2) (@eq Elt x (injdroite x0))) (x1 : Elt) (_ : and (dans x1 V1) (@eq Elt x (injgauche x1))), dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
intros x2 temp; elim temp; clear temp; intros dans_x2_V2 egal_x2.
(* Goal: forall (x0 : Elt) (_ : and (dans x0 V1) (@eq Elt x (injgauche x0))), dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
intros x1 temp; elim temp; clear temp; intros dans_x1_V1 egal_x1.
(* Goal: dans x empty *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
absurd (zero = un).
(* Goal: not (@eq Elt zero un) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
unfold zero, un in |- *.
(* Goal: not (@eq Elt (natural O) (natural (S O))) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
red in |- *.
(* Goal: forall _ : @eq Elt (natural O) (natural (S O)), False *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
intro.
(* Goal: False *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
cut (0 = 1 :>nat).
(* Goal: forall _ : @eq nat O (S O), False *)
(* Goal: @eq nat O (S O) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
change (0 <> 1 :>nat) in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: @eq nat O (S O) *)
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
change (natural_inv (natural 0) = natural_inv (natural 1) :>nat) in |- *.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply (f_equal natural_inv); assumption.
(* Goal: @eq Elt zero un *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
apply couple_couple_inv2 with x1 x2.
(* Goal: @eq Elt (couple x1 zero) (couple x2 un) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V2) (@eq Elt x (injdroite y))) *)
(* Goal: @ex Elt (fun y : Elt => and (dans y V1) (@eq Elt x (injgauche y))) *)
(* Goal: @eq Ensf (map injdroite V2) (map (injproducd V2) V2) *)
(* Goal: @eq Ensf (map injgauche V1) (map (injproducg V1) V1) *)
replace (couple x1 zero) with x.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply dans_map; assumption.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply dans_map; assumption.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.

Hint Resolve inter_V1'_V2'_empty.



Lemma egal_LG_u_1'_2' :
 l_egal (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')).
(* Goal: l_egal (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) *)
unfold Ru, Vu, C', Gim in |- *.
(* Goal: l_egal (LG X (@fst Ensf (prod Ensf Elt) (Gunion_disj_p V1' R1' S1' V2' R2' S2' S')) (@fst Ensf Elt (@snd Ensf (prod Ensf Elt) (Gunion_disj_p V1' R1' S1' V2' R2' S2' S'))) S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) *)
apply Gunion_disj_LG.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.
Qed.
Hint Resolve egal_LG_u_1'_2'.



Theorem union_is_LCF :
 l_egal (LG X Vu Ru S') (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)).
(* Goal: l_egal (LG X Vu Ru S') (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) *)
elimtype (l_egal (LG X V1 R1 S1) (LG X V1' R1' S1')).
(* Goal: forall (_ : l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (_ : l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)), l_egal (LG X Vu Ru S') (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
elimtype (l_egal (LG X V2 R2 S2) (LG X V2' R2' S2')).
elimtype
 (l_egal (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))).

intros incl_i_u_1'_2' incl_u_1'_2'_u_i incl_2_2' incl_2'_2 incl_1_1'
 incl_1'_1.

(* Goal: l_egal (LG X Vu Ru S') (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
unfold l_egal in |- *; split; unfold l_inclus in |- *.
(* Goal: forall (w : Word) (_ : LG X Vu Ru S' w), lunion (LG X V1 R1 S1) (LG X V2 R2 S2) w *)
(* Goal: forall (w : Word) (_ : lunion (LG X V1 R1 S1) (LG X V2 R2 S2) w), LG X Vu Ru S' w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
	intros w LG_Ru_w.
	elimtype (lunion (LG X V1' R1' S1') (LG X V2' R2' S2') w);
(* Goal: lunion (LG X V1' R1' S1') (LG X V2' R2' S2') w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
  unfold lunion in |- *.
(* Goal: forall _ : LG X V1' R1' S1' w, or (LG X V1 R1 S1 w) (LG X V2 R2 S2 w) *)
(* Goal: forall _ : LG X V2' R2' S2' w, or (LG X V1 R1 S1 w) (LG X V2 R2 S2 w) *)
(* Goal: or (LG X V1' R1' S1' w) (LG X V2' R2' S2' w) *)
(* Goal: forall (w : Word) (_ : lunion (LG X V1 R1 S1) (LG X V2 R2 S2) w), LG X Vu Ru S' w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
intro Hyp; apply or_introl.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply incl_1'_1; assumption.

(* Goal: forall _ : LG X V2' R2' S2' w, or (LG X V1 R1 S1 w) (LG X V2 R2 S2 w) *)
(* Goal: or (LG X V1' R1' S1' w) (LG X V2' R2' S2' w) *)
(* Goal: forall (w : Word) (_ : lunion (LG X V1 R1 S1) (LG X V2 R2 S2) w), LG X Vu Ru S' w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
intro Hyp; apply or_intror.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply incl_2'_2; assumption.

(* Goal: or (LG X V1' R1' S1' w) (LG X V2' R2' S2' w) *)
(* Goal: forall (w : Word) (_ : lunion (LG X V1 R1 S1) (LG X V2 R2 S2) w), LG X Vu Ru S' w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
change (lunion (LG X V1' R1' S1') (LG X V2' R2' S2') w) in |- *.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply incl_i_u_1'_2'; assumption.

(* Goal: forall (w : Word) (_ : lunion (LG X V1 R1 S1) (LG X V2 R2 S2) w), LG X Vu Ru S' w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
intros w lunion_LG_1_2_w.
(* Goal: LG X Vu Ru S' w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
apply incl_u_1'_2'_u_i.
(* Goal: lunion (LG X V1' R1' S1') (LG X V2' R2' S2') w *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
unfold lunion in |- *.
(* Goal: or (LG X V1' R1' S1' w) (LG X V2' R2' S2' w) *)
(* Goal: and (l_inclus (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2'))) (l_inclus (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')) (LG X Vu Ru S')) *)
(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
elim lunion_LG_1_2_w; intro LG_w.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply or_introl; apply incl_1_1'; assumption.
(* Goal: dans S' (map (fun e : Elt => couple e un) V2) *)
(* Goal: @eq Ensf (map injdroite V2) V2' *)
apply or_intror; apply incl_2_2'; assumption.

change
  (l_egal (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')))
 in |- *.

(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

(* Goal: and (l_inclus (LG X V2 R2 S2) (LG X V2' R2' S2')) (l_inclus (LG X V2' R2' S2') (LG X V2 R2 S2)) *)
(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
change (l_egal (LG X V2 R2 S2) (LG X V2' R2' S2')) in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

(* Goal: and (l_inclus (LG X V1 R1 S1) (LG X V1' R1' S1')) (l_inclus (LG X V1' R1' S1') (LG X V1 R1 S1)) *)
change (l_egal (LG X V1 R1 S1) (LG X V1' R1' S1')) in |- *.
(* Goal: l_egal (LG X V1 R1 S1) (LG X V1' R1' S1') *)
auto.

Qed.


End gram5.