(* Properties on relocation *************************************************)
lemma cir_lift: ∀K,T. K ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
(* Properties on relocation *************************************************)
lemma cir_lift: ∀K,T. K ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
-lemma cir_inv_lift: ∀L,U. L ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma cir_inv_lift: ∀L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →