∀T2. ⦃L1,T1⦄ ⊆ ⦃L2,T2⦄ → ⦃L1.ⓧ,U1⦄ ⊆ ⦃L2,T2⦄.
#T1 #U1 #HTU1 #L1 #L2 #H1L #T2
* #n #m #f #g #Hf #Hg #H2L #Hfg
∀T2. ⦃L1,T1⦄ ⊆ ⦃L2,T2⦄ → ⦃L1.ⓧ,U1⦄ ⊆ ⦃L2,T2⦄.
#T1 #U1 #HTU1 #L1 #L2 #H1L #T2
* #n #m #f #g #Hf #Hg #H2L #Hfg
∀T1. ⦃L1,T1⦄ ⊆ ⦃L2,T2⦄ → ⦃L1,T1⦄ ⊆ ⦃L2.ⓧ,U2⦄.
#L1 #L2 #HL21 #T2 #U2 #HTU2 #T1
* #n #m #f #g #Hf #Hg #H2L #Hfg
∀T1. ⦃L1,T1⦄ ⊆ ⦃L2,T2⦄ → ⦃L1,T1⦄ ⊆ ⦃L2.ⓧ,U2⦄.
#L1 #L2 #HL21 #T2 #U2 #HTU2 #T1
* #n #m #f #g #Hf #Hg #H2L #Hfg
qed-.
lemma fsle_lifts_SO_sn: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1,V1⦄ ⊆ ⦃K2,V2⦄ →
qed-.
lemma fsle_lifts_SO_sn: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1,V1⦄ ⊆ ⦃K2,V2⦄ →
- â\88\80W1. â¬\86*[1] V1 ≘ W1 → ∀I1,I2. ⦃K1.ⓘ{I1},W1⦄ ⊆ ⦃K2.ⓑ{I2}V2,#O⦄.
+ â\88\80W1. â\87§*[1] V1 ≘ W1 → ∀I1,I2. ⦃K1.ⓘ{I1},W1⦄ ⊆ ⦃K2.ⓑ{I2}V2,#O⦄.
qed.
lemma fsle_lifts_SO: ∀K1,K2. |K1| = |K2| → ∀T1,T2. ⦃K1,T1⦄ ⊆ ⦃K2,T2⦄ →
qed.
lemma fsle_lifts_SO: ∀K1,K2. |K1| = |K2| → ∀T1,T2. ⦃K1,T1⦄ ⊆ ⦃K2,T2⦄ →
∀I1,I2. ⦃K1.ⓘ{I1},U1⦄ ⊆ ⦃K2.ⓘ{I2},U2⦄.
#K1 #K2 #HK #T1 #T2
* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
∀I1,I2. ⦃K1.ⓘ{I1},U1⦄ ⊆ ⦃K2.ⓘ{I2},U2⦄.
#K1 #K2 #HK #T1 #T2
* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
∀I1,I2,L1,L2,V1,V2,U2. ⦃L1.ⓑ{I1}V1,U1⦄ ⊆ ⦃L2.ⓑ{I2}V2,U2⦄ →
∀p. ⦃L1,T1⦄ ⊆ ⦃L2,ⓑ{p,I2}V2.U2⦄.
#T1 #U1 #HTU1 #I1 #I2 #L1 #L2 #V1 #V2 #U2
∀I1,I2,L1,L2,V1,V2,U2. ⦃L1.ⓑ{I1}V1,U1⦄ ⊆ ⦃L2.ⓑ{I2}V2,U2⦄ →
∀p. ⦃L1,T1⦄ ⊆ ⦃L2,ⓑ{p,I2}V2.U2⦄.
#T1 #U1 #HTU1 #I1 #I2 #L1 #L2 #V1 #V2 #U2