-lemma lsubr_fwd_drop2_bind: ∀L1,L2. L1 ⫃ L2 →
- â\88\80I,K2,W,s,i. â\87©[s, 0, i] L2 ≡ K2.ⓑ{I}W →
- (â\88\83â\88\83K1. K1 â«\83 K2 & â\87©[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
- â\88\83â\88\83K1,V. K1 â«\83 K2 & â\87©[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
+lemma lsubr_fwd_drop2_pair: ∀L1,L2. L1 ⫃ L2 →
+ â\88\80I,K2,W,s,i. â¬\87[s, 0, i] L2 ≡ K2.ⓑ{I}W →
+ (â\88\83â\88\83K1. K1 â«\83 K2 & â¬\87[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
+ â\88\83â\88\83K1,V. K1 â«\83 K2 & â¬\87[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.