-lemma fsle_inv_lifts_sn: â\88\80T1,U1. â¬\86*[1] T1 ≘ U1 →
- ∀I1,I2,L1,L2,V1,V2,U2. ⦃L1.ⓑ{I1}V1,U1⦄ ⊆ ⦃L2.ⓑ{I2}V2, U2⦄ →
- ∀p. ⦃L1, T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.U2⦄.
+lemma fsle_inv_lifts_sn: â\88\80T1,U1. â\87§*[1] T1 ≘ U1 →
+ ∀I1,I2,L1,L2,V1,V2,U2. ⦃L1.ⓑ{I1}V1,U1⦄ ⊆ ⦃L2.ⓑ{I2}V2,U2⦄ →
+ ∀p. ⦃L1,T1⦄ ⊆ ⦃L2,ⓑ{p,I2}V2.U2⦄.