proposition: Lemma egal_LG_2_2' : l_egal (LG X V2 R2 S2) (LG X V2' R2' S2').
proof: Proof. pattern X at 2 in |- *. replace X with X2'. unfold X2', V2', R2', S2', GGG2, GG2, G2 in |- *. apply egal_LG. auto. auto. red in |- *; auto. unfold X2' in |- *; simpl in |- *. apply map_Id. red in |- *. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4