-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_unit2: ∀I,L1,K2. L1 ⫃ K2.ⓤ{I} →
+ ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓤ{I}
+ | ∃∃J,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J}V.
+#I #L1 #K2 #H elim (lsubr_inv_bind2 … H) -H *
+[ /3 width=3 by ex2_intro, or_introl/
+| #K1 #W #V #_ #_ #H destruct
+| #I1 #I2 #K1 #V #HK12 #H1 #H2 destruct /3 width=5 by ex2_3_intro, or_intror/