proposition: Theorem union_is_LCF : l_egal (LG X Vu Ru S') (lunion (LG X V1 R1 S1) (LG X V2 R2 S2)).
proof: Proof. elimtype (l_egal (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. unfold l_egal in |- *; split; unfold l_inclus in |- *. intros w LG_Ru_w. elimtype (lunion (LG X V1' R1' S1') (LG X V2' R2' S2') w); unfold lunion in |- *. intro Hyp; apply or_introl. apply incl_1'_1; assumption. intro Hyp; apply or_intror. apply incl_2'_2; assumption. change (lunion (LG X V1' R1' S1') (LG X V2' R2' S2') w) in |- *. apply incl_i_u_1'_2'; assumption. intros w lunion_LG_1_2_w. apply incl_u_1'_2'_u_i. unfold lunion in |- *. elim lunion_LG_1_2_w; intro LG_w. apply or_introl; apply incl_1_1'; assumption. 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 |- *. auto. change (l_egal (LG X V2 R2 S2) (LG X V2' R2' S2')) in |- *. auto. change (l_egal (LG X V1 R1 S1) (LG X V1' R1' S1')) in |- *. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4