∀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 →