-lemma lsubr_fwd_ldrop2_bind: ∀L1,L2. L1 ⫃ L2 →
- ∀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.
-#L1 #L2 #H elim H -L1 -L2
-[ #L #I #K2 #W #s #i #H
- elim (ldrop_inv_atom1 … H) -H #H destruct
-| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #s #i #H
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=3 by ldrop_pair, ex2_intro, or_introl/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 *
- /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
- ]
-| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #s #i #H
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=4 by ldrop_pair, ex3_2_intro, or_intror/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 *
- /4 width=4 by ldrop_drop_lt, ex3_2_intro, ex2_intro, or_introl, or_intror/
- ]
+lemma lsubr_inv_abst2: ∀L1,K2,W. L1 ⫃ K2.ⓛW →
+ (∃∃K1. K1 ⫃ K2 & L1 = K1.ⓛW) ∨
+ ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V.
+#L1 #K2 #W #H elim (lsubr_inv_pair2 … H) -H *
+[ #K1 #HK12 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #K1 #V1 #HK12 #H #_ destruct /3 width=4 by ex2_2_intro, or_intror/