-lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fle_compatible R1 →
- ∀L1,L2,V. L1 ⪤*[R1, V] L2 → ∀I,T.
- ∃∃L. L1 ⪤*[R1, ②{I}V.T] L & L ⪤*[R2, V] L2.
-#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T
-[ elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg
- elim (frees_inv_bind … Hg) #y1 #y2 #H #_ #Hy
-| elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg
- elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy
-]
-lapply(frees_mono … H … Hf) -H #H1
-lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy
-lapply (sor_inv_sle_sn … Hy) -y2 #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
-lapply (sle_lexs_trans … HL1 … Hfg) // #H
-elim (frees_lexs_conf … Hf … H) -Hf -H
-/4 width=7 by sle_lexs_trans, ex2_intro/
-qed-.
-
-lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fle_compatible R1 →
- ∀L1,L2,T. L1 ⪤*[R1, T] L2 → ∀I,V.
- ∃∃L. L1 ⪤*[R1, ⓕ{I}V.T] L & L ⪤*[R2, T] L2.
-#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V
-elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg
-elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy
-lapply(frees_mono … H … Hf) -H #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
-lapply (sle_lexs_trans … HL1 … Hfg) // #H
-elim (frees_lexs_conf … Hf … H) -Hf -H
-/4 width=7 by sle_lexs_trans, ex2_intro/
-qed-.
-
-lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fle_compatible R1 →
- ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤*[R1, T] L2 → ∀p.
- ∃∃L,V. L1 ⪤*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤*[R2, T] L2 & R1 L1 V1 V.
-#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p
-elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg
-elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy
-lapply(frees_mono … H … Hf) -H #H2
-lapply (tl_eq_repl … H2) -H2 #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
-lapply (sle_lexs_trans … H … Hfg) // #H0
-elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H
-elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct
-elim (frees_lexs_conf … Hf … H0) -Hf -H0
-/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/
-qed-.
-
-lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fle_compatible R1 →
- ∀L1,L2,T. L1.ⓧ ⪤*[R1, T] L2 → ∀p,I,V.
- ∃∃L. L1 ⪤*[R1, ⓑ{p,I}V.T] L & L.ⓧ ⪤*[R2, T] L2.
-#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #p #I #V
-elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg
-elim (frees_inv_bind_void … Hg) #y1 #y2 #_ #H #Hy
-lapply(frees_mono … H … Hf) -H #H2
-lapply (tl_eq_repl … H2) -H2 #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
-elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
-lapply (sle_lexs_trans … H … Hfg) // #H0
-elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H
-elim (ext2_inv_unit_sn … H) -H #H destruct
-elim (frees_lexs_conf … Hf … H0) -Hf -H0
-/4 width=7 by sle_lexs_trans, ex2_intro/ (* note: 2 ex2_intro *)
-qed-.
-