-lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄ → ∀K,s,d,e. ⬇[s, d, e] L ≡ K →
- ∀T. ⬆[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
+lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄ → ∀K,s,l,m. ⬇[s, l, m] L ≡ K →
+ ∀T. ⬆[l, m] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.