definition co_dedropable_sn: predicate (rtmap → relation lenv) ≝
λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀f1,K2. R f1 K1 K2 →
∀f2. f ~⊚ f1 ≡ f2 →
definition co_dedropable_sn: predicate (rtmap → relation lenv) ≝
λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀f1,K2. R f1 K1 K2 →
∀f2. f ~⊚ f1 ≡ f2 →