proposition: Lemma Gunion_disj_LG_inclus4 : l_inclus (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)) (LG X Vu Ru S).
proof: Proof. unfold l_inclus, lunion in |- *. intros w temp; elim temp; clear temp; intro LG_w. apply Gunion_disj_LG_inclus2; assumption. apply Gunion_disj_LG_inclus3; assumption. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3