- λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀L2,u2. R u2 L1 L2 →
- ∀u1. f ⊚ u1 ≡ u2 →
- ∃∃K2. R u1 K1 K2 & ⬇*[c, f] L2 ≡ K2.
+ λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀L2,f2. R f2 L1 L2 →
+ ∀f1. f ⊚ f1 ≡ f2 →
+ ∃∃K2. R f1 K1 K2 & ⬇*[c, f] L2 ≡ K2.
+
+definition dropable_dx: predicate (rtmap → relation lenv) ≝
+ λR. ∀L1,L2,f2. R f2 L1 L2 →
+ ∀K2,c,f. ⬇*[c, f] L2 ≡ K2 → 𝐔⦃f⦄ →
+ ∀f1. f ⊚ f1 ≡ f2 →
+ ∃∃K1. ⬇*[c, f] L1 ≡ K1 & R f1 K1 K2.
+
+definition dedropable_sn: predicate (rtmap → relation lenv) ≝
+ λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀K2,f1. R f1 K1 K2 →
+ ∀f2. f ⊚ f1 ≡ f2 →
+ ∃∃L2. R f2 L1 L2 & ⬇*[c, f] L2 ≡ K2 & L1 ≡[f] L2.