-theorem fsle_bind: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
- ∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
- ∀p. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄.
+theorem fsle_bind: ∀L1,L2,V1,V2. ⦃L1,V1⦄ ⊆ ⦃L2,V2⦄ →
+ ∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1,T1⦄ ⊆ ⦃L2.ⓑ{I2}V2,T2⦄ →
+ ∀p. ⦃L1,ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2,ⓑ{p,I2}V2.T2⦄.