-definition dropable_dx: predicate (relation3 lenv term term) ≝
- λR. ∀L1,L2,U. L1 ⪤*[R, U] L2 →
- ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U →
- ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⪤*[R, T] K2.
+definition f_dropable_dx: predicate (relation3 lenv term term) ≝
+ λR. ∀L1,L2,U. L1 ⪤*[R, U] L2 →
+ ∀b,f,K2. ⬇*[b, f] L2 ≘ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≘ U →
+ ∃∃K1. ⬇*[b, f] L1 ≘ K1 & K1 ⪤*[R, T] K2.
+
+definition f_transitive_next: relation3 … ≝ λR1,R2,R3.
+ ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≘ f →
+ ∀g,I,K,n. ⬇*[n] L ≘ K.ⓘ{I} → ↑g = ⫱*[n] f →
+ lexs_transitive (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.