(* Advanced inversion lemmas ************************************************)
-lemma cix_inv_append_sn: ∀h,g,L,K,T. ⦃h, K @@ L⦄ ⊢ 𝐈[g]⦃T⦄ → ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄.
+lemma cix_inv_append_sn: ∀h,g,L,K,T. ⦃h, K @@ L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄.
/3 width=1/ qed-.
-lemma cix_inv_tix: ∀h,g,L,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃T⦄ → ⦃h, ⋆⦄ ⊢ 𝐈[g]⦃T⦄.
+lemma cix_inv_tix: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃h, ⋆⦄ ⊢ 𝐈[h, g]⦃T⦄.
/3 width=1/ qed-.