proposition: Lemma egal_LG_u_1'_2' : l_egal (LG X Vu Ru S') (lunion (LG X V1' R1' S1') (LG X V2' R2' S2')).
proof: Proof. unfold Ru, Vu, C', Gim in |- *. apply Gunion_disj_LG. auto. auto. auto. auto. auto. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4