qed-.
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.
+ â\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.
#L1 #L2 #H elim H -L1 -L2
[ #L #I #K2 #W #s #i #H
elim (drop_inv_atom1 … H) -H #H destruct
qed-.
lemma lsubr_fwd_drop2_abbr: ∀L1,L2. L1 ⫃ L2 →
- â\88\80K2,V,s,i. â\87©[s, 0, i] L2 ≡ K2.ⓓV →
- â\88\83â\88\83K1. K1 â«\83 K2 & â\87©[s, 0, i] L1 ≡ K1.ⓓV.
+ â\88\80K2,V,s,i. â¬\87[s, 0, i] L2 ≡ K2.ⓓV →
+ â\88\83â\88\83K1. K1 â«\83 K2 & â¬\87[s, 0, i] L1 ≡ K1.ⓓV.
#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_drop2_pair … HL12 … HLK2) -L2 // *
#K1 #W #_ #_ #H destruct
qed-.