- ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W →
- (∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨
- ∃∃K1,V. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
+ ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W →
+ (∃∃K1. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
+ ∃∃K1,V. K1 ⊑ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.