(* Main properties on context-sensitive irreducible terms *******************)
-theorem cir_cnr: ∀L,T. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
-/2 width=3 by cpr_fwd_cir/ qed.
+theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄.
+/2 width=4 by cpr_fwd_cir/ qed.
(* Main inversion lemmas on context-sensitive irreducible terms *************)
-theorem cnr_inv_cir: ∀L,T. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄.
-/2 width=4 by cnr_inv_crr/ qed-.
+theorem cnr_inv_cir: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄.
+/2 width=5 by cnr_inv_crr/ qed-.