definition tc_dedropable_sn: predicate (relation3 lenv term term) ≝
λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
∀K2,T. K1 ⪤**[R, T] K2 → ∀U. ⬆*[f] T ≡ U →
definition tc_dedropable_sn: predicate (relation3 lenv term term) ≝
λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
∀K2,T. K1 ⪤**[R, T] K2 → ∀U. ⬆*[f] T ≡ U →