∀L2,U. L1 ⪤*[R,U] L2 → ∀T. ⇧*[f] T ≘ U →
∃∃K2. K1 ⪤*[R,T] K2 & ⇩*[b,f] L2 ≘ K2.
definition tc_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 tc_f_dropable_dx: predicate (relation3 lenv term term) ≝
λR. ∀L1,L2,U. L1 ⪤*[R,U] L2 →