proposition: Lemma egal_LG_1_1' : l_egal (LG X V1 R1 S1) (LG X V1' R1' S1').
proof: Proof. pattern X at 2 in |- *. replace X with X1'. unfold X1', V1', R1', S1', GGG1, GG1, G1 in |- *. apply egal_LG. auto. auto. red in |- *; auto. unfold X1' in |- *; simpl in |- *. apply map_Id. red in |- *. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4