- ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
- ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
-#d1 #e1 #L #L1 #H1 #e2 #K2 #I #V2 #H2 #He2d1
-elim (ldrop_conf_le … H1 … H2 ?) -L [2: /2 width=2/] #K #HL1K #HK2
-elim (ldrop_inv_skip1 … HK2 ?) -HK2 [2: /2 width=1/] #K1 #V1 #HK21 #HV12 #H destruct /2 width=5/
-qed.
+ ∃∃K1,V1. ⇩[s2, 0, e2] L1 ≡ K1.ⓑ{I}V1 &
+ ⇩[s1, d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
+#L #L1 #s1 #d1 #e1 #H1 #I #K2 #V2 #s2 #e2 #H2 #He2d1
+elim (ldrop_conf_le … H1 … H2) -L /2 width=2 by lt_to_le/ #K #HL1K #HK2
+elim (ldrop_inv_skip1 … HK2) -HK2 /2 width=1 by lt_plus_to_minus_r/
+#K1 #V1 #HK21 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+(* Note: apparently this was missing in basic_1 *)
+lemma ldrop_trans_lt: ∀L1,L,s1,d1,e1. ⇩[s1, d1, e1] L1 ≡ L →
+ ∀I,L2,V2,s2,e2. ⇩[s2, 0, e2] L ≡ L2.ⓑ{I}V2 →
+ e2 < d1 → let d ≝ d1 - e2 - 1 in
+ ∃∃L0,V0. ⇩[s2, 0, e2] L1 ≡ L0.ⓑ{I}V0 &
+ ⇩[s1, d, e1] L0 ≡ L2 & ⇧[d, e1] V2 ≡ V0.
+#L1 #L #s1 #d1 #e1 #HL1 #I #L2 #V2 #s2 #e2 #HL2 #Hd21
+elim (ldrop_trans_le … HL1 … HL2) -L /2 width=1 by lt_to_le/ #L0 #HL10 #HL02
+elim (ldrop_inv_skip2 … HL02) -HL02 /2 width=1 by lt_plus_to_minus_r/ #L #V1 #HL2 #HV21 #H destruct /2 width=5 by ex3_2_intro/
+qed-.