-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,d,e. ⇩[s, d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.