- ∀I,K2,W,c,f. 𝐔⦃f⦄ → ⬇*[c, f] L2 ≡ K2.ⓑ{I}W →
- (∃∃K1. K1 ⫃ K2 & ⬇*[c, f] L1 ≡ K1.ⓑ{I}W) ∨
- ∃∃K1,V. K1 ⫃ K2 & ⬇*[c, f] L1 ≡ K1.ⓓⓝW.V & I = Abst.
+ ∀b,f,I,K2,W. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2.ⓑ{I}W →
+ (∃∃K1. K1 ⫃ K2 & ⬇*[b, f] L1 ≡ K1.ⓑ{I}W) ∨
+ ∃∃K1,V. K1 ⫃ K2 & ⬇*[b, f] L1 ≡ K1.ⓓⓝW.V & I = Abst.