-lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
+lemma lleq_fwd_drop_sn: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
-lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
+lemma lleq_fwd_drop_dx: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
L1 ≡[ⓑ{a,I}V.T, d] L2 → L1 ≡[V, d] L2.
lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
L1 ≡[ⓑ{a,I}V.T, d] L2 → L1 ≡[V, d] L2.