-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❫.