- λR. ∀L,U1,U2. R L U1 U2 → ∀K,s,t. ⬇*[s, t] L ≡ K →
- ∀T1. ⬆*[t] T1 ≡ U1 →
- ∃∃T2. ⬆*[t] T2 ≡ U2 & R K T1 T2.
-
-definition dropable_sn: predicate (relation lenv) ≝
- λR. ∀L1,K1,s,t. ⬇*[s, t] L1 ≡ K1 → ∀L2. R L1 L2 →
- ∃∃K2. R K1 K2 & ⬇*[s, t] L2 ≡ K2.
-(*
-definition dropable_dx: predicate (relation lenv) ≝
- λR. ∀L1,L2. R L1 L2 → ∀K2,s,m. ⬇[s, 0, m] L2 ≡ K2 →
- ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & R K1 K2.
-*)
+ λR. ∀L,U1,U2. R L U1 U2 → ∀K,c,f. ⬇*[c, f] L ≡ K →
+ ∀T1. ⬆*[f] T1 ≡ U1 →
+ ∃∃T2. ⬆*[f] T2 ≡ U2 & R K T1 T2.
+
+definition dropable_sn: predicate (rtmap → relation lenv) ≝
+ λ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.
+