∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⇧*[f] T ≘ U →
∃∃K2. K1 ⪤[R,T] K2 & ⇩*[b,f] L2 ≘ K2.
definition f_dropable_dx: predicate (relation3 lenv term term) ≝
λR. ∀L1,L2,U. L1 ⪤[R,U] L2 →
∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⇧*[f] T ≘ U →
∃∃K2. K1 ⪤[R,T] K2 & ⇩*[b,f] L2 ≘ K2.
definition f_dropable_dx: predicate (relation3 lenv term term) ≝
λR. ∀L1,L2,U. L1 ⪤[R,U] L2 →