diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v
index 9cf3fce..57730c9 100644
--- a/theories/Core/Completeness/NatCases.v
+++ b/theories/Core/Completeness/NatCases.v
@@ -414,8 +414,8 @@ Proof.
     | _: env_relΓ ρ ?ρ0 |- _ =>
         rename ρ0 into ρ'
     end.
-    assert {{ Dom ⇑ ℕ m ≈ ⇑ ℕ m' ∈ per_nat }} by (econstructor; eassumption).
-    assert {{ Dom ρ ↦ ⇑ ℕ m ≈ ρ' ↦ ⇑ ℕ m' ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; mauto).
+    assert {{ Dom ⇑ a m ≈ ⇑ b m' ∈ per_nat }} by (econstructor; eassumption).
+    assert {{ Dom ρ ↦ ⇑ a m ≈ ρ' ↦ ⇑ b m' ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; mauto).
     apply_relation_equivalence.
     (on_all_hyp: fun H => directed destruct (H _ _ HinΓℕ)).
     destruct_by_head per_univ.
@@ -594,8 +594,8 @@ Proof.
         rename ρ1 into ρσ;
         rename ρ2 into ρ'σ
     end.
-    assert {{ Dom ⇑ ℕ m ≈ ⇑ ℕ m' ∈ per_nat }} by (econstructor; eassumption).
-    assert {{ Dom ρσ ↦ ⇑ ℕ m ≈ ρ'σ ↦ ⇑ ℕ m' ∈ env_relΔℕ }} as HinΔℕ by (apply_relation_equivalence; mauto).
+    assert {{ Dom ⇑ a m ≈ ⇑ b m' ∈ per_nat }} by (econstructor; eassumption).
+    assert {{ Dom ρσ ↦ ⇑ a m ≈ ρ'σ ↦ ⇑ b m' ∈ env_relΔℕ }} as HinΔℕ by (apply_relation_equivalence; mauto).
     apply_relation_equivalence.
     (on_all_hyp: fun H => directed destruct (H _ _ HinΔℕ)).
     destruct_by_head per_univ.
diff --git a/theories/Core/Semantic/Evaluation/Definitions.v b/theories/Core/Semantic/Evaluation/Definitions.v
index b0ff492..174a772 100644
--- a/theories/Core/Semantic/Evaluation/Definitions.v
+++ b/theories/Core/Semantic/Evaluation/Definitions.v
@@ -50,8 +50,8 @@ with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
      {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ms }} )
 | eval_natrec_neut :
   `( {{ ⟦ MZ ⟧ ρ ↘ mz }} ->
-     {{ ⟦ A ⟧ ρ ↦ ⇑ ℕ m ↘ a }} ->
-     {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ⇑ a (rec m under ρ return A | zero -> mz | succ -> MS end) }} )
+     {{ ⟦ A ⟧ ρ ↦ ⇑ b m ↘ a }} ->
+     {{ rec ⇑ b m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ⇑ a (rec m under ρ return A | zero -> mz | succ -> MS end) }} )
 where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' ρ '↘' r" := (eval_natrec A MZ MS m ρ r) (in custom judg)
 with eval_app : domain -> domain -> domain -> Prop :=
 | eval_app_fn :
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index ed39920..1b22fc4 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -66,7 +66,7 @@ Inductive per_nat : relation domain :=
      {{ Dom succ m ≈ succ n ∈ per_nat }} }
 | per_nat_neut :
   `{ {{ Dom m ≈ n ∈ per_bot }} ->
-     {{ Dom ⇑ ℕ m ≈ ⇑ ℕ n ∈ per_nat }} }
+     {{ Dom ⇑ a m ≈ ⇑ b n ∈ per_nat }} }
 .
 #[export]
 Hint Constructors per_nat : mcltt.
diff --git a/theories/Core/Semantic/Readback/Definitions.v b/theories/Core/Semantic/Readback/Definitions.v
index eaff877..a958bde 100644
--- a/theories/Core/Semantic/Readback/Definitions.v
+++ b/theories/Core/Semantic/Readback/Definitions.v
@@ -20,7 +20,7 @@ Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
      {{ Rnf ⇓ ℕ (succ m) in s ↘ succ M }} )
 | read_nf_nat_neut :
   `( {{ Rne m in s ↘ M }} ->
-     {{ Rnf ⇓ ℕ (⇑ ℕ m) in s ↘ ⇑ M }} )
+     {{ Rnf ⇓ ℕ (⇑ a m) in s ↘ ⇑ M }} )
 | read_nf_fn :
   `( (** Normal form of arg type *)
      {{ Rtyp a in s ↘ A }} ->
diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index 3dc2aa7..1e6220e 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -41,7 +41,7 @@ Inductive glu_nat : ctx -> exp -> domain -> Prop :=
 | glu_nat_neut :
   `{ per_bot m m ->
      (forall {Δ σ M'}, {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : ℕ }}) ->
-     glu_nat Γ M d{{{ ⇑ ℕ m }}} }.
+     glu_nat Γ M d{{{ ⇑ a m }}} }.
 
 #[export]
 Hint Constructors glu_nat : mcltt.
diff --git a/theories/Core/Soundness/NatCases.v b/theories/Core/Soundness/NatCases.v
index 90da484..3f8acbb 100644
--- a/theories/Core/Soundness/NatCases.v
+++ b/theories/Core/Soundness/NatCases.v
@@ -352,7 +352,7 @@ Qed.
 #[local]
 Hint Resolve cons_glu_sub_pred_q_nat_helper : mcltt.
 
-Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M m σ ρ am P El},
+Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M a m σ ρ am P El},
     {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
     {{ Γ, ℕ ⊩ A : Type@i }} ->
     {{ Γ ⊩ A[Id,,zero] : Type@i }} ->
@@ -362,10 +362,10 @@ Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M m σ ρ am
     {{ Dom m ≈ m ∈ per_bot }} ->
     (forall Δ' τ V, {{ Δ' ⊢w τ : Δ }} -> {{ Rne m in length Δ' ↘ V }} -> {{ Δ' ⊢ M[τ] ≈ V : ℕ }}) ->
     {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
-    {{ ⟦ A ⟧ ρ ↦ ⇑ ℕ m ↘ am }} ->
+    {{ ⟦ A ⟧ ρ ↦ ⇑ a m ↘ am }} ->
     {{ DG am ∈ glu_univ_elem i ↘ P ↘ El }} ->
     exists r,
-      {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
+      {{ rec ⇑ a m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
         {{ Δ ⊢ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M] ® r ∈ El }}.
 Proof.
   intros * ? HA ? HMZ ? HMS **.
@@ -380,7 +380,7 @@ Proof.
   invert_glu_rel_exp HA.
   pose (SbΓℕA := cons_glu_sub_pred i {{{ Γ, ℕ }}} A SbΓℕ).
   assert {{ EG Γ, ℕ, A ∈ glu_ctx_env ↘ SbΓℕA }} by (econstructor; mauto 3; reflexivity).
-  assert {{ Δ ⊢s σ,,M ® ρ ↦ ⇑ ℕ m ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3).
+  assert {{ Δ ⊢s σ,,M ® ρ ↦ ⇑ a m ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3).
   assert {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} by mauto 2.
   invert_glu_rel_exp HMS.
   destruct_glu_rel_exp_with_sub.
@@ -402,7 +402,7 @@ Proof.
   assert {{ ⊢ Δ, ℕ }} by mauto 3.
   assert {{ Δ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3.
   assert {{ ⊢ Δ, ℕ, A[q σ] }} by mauto 2.
-  assert {{ Δ ⊢ M : ℕ }} by mauto 3.
+  unshelve assert {{ Δ ⊢ M : ℕ }} by mauto 3; [constructor |].
   assert {{ Δ ⊢ ℕ : Type@0 }} by mauto 3.
   assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} by mauto 3.
   assert {{ Δ ⊢ M : ℕ[σ] }} by mauto 3.
diff --git a/theories/Extraction/Evaluation.v b/theories/Extraction/Evaluation.v
index 65f81e5..50c04d5 100644
--- a/theories/Extraction/Evaluation.v
+++ b/theories/Extraction/Evaluation.v
@@ -48,8 +48,8 @@ with eval_natrec_order : exp -> exp -> exp -> domain -> env -> Prop :=
      eval_natrec_order A MZ MS d{{{ succ b }}} p )
 | eno_neut :
   `( eval_exp_order MZ p ->
-     eval_exp_order A d{{{ p ↦ ⇑ ℕ m }}} ->
-     eval_natrec_order A MZ MS d{{{ ⇑ ℕ m }}} p )
+     eval_exp_order A d{{{ p ↦ ⇑ a m }}} ->
+     eval_natrec_order A MZ MS d{{{ ⇑ a m }}} p )
 
 with eval_app_order : domain -> domain -> Prop :=
 | eao_fn :
@@ -146,9 +146,9 @@ with eval_natrec_impl A MZ MS m p (H : eval_natrec_order A MZ MS m p) : { d | ev
     let (mr, Hmr) := eval_natrec_impl A MZ MS m p _ in
     let (r, Hr) := eval_exp_impl MS d{{{ p ↦ m ↦ mr }}} _ in
     exist _ r _
-| A, MZ, MS, d{{{ ⇑ ℕ m }}} , p, H =>
+| A, MZ, MS, d{{{ ⇑ a m }}} , p, H =>
     let (mz, Hmz) := eval_exp_impl MZ p _ in
-    let (mA, HmA) := eval_exp_impl A d{{{ p ↦ ⇑ ℕ m }}} _ in
+    let (mA, HmA) := eval_exp_impl A d{{{ p ↦ ⇑ a m }}} _ in
     exist _ d{{{ ⇑ mA (rec m under p return A | zero -> mz | succ -> MS end) }}} _
 
 with eval_app_impl m n (H : eval_app_order m n) : { d | eval_app m n d } by struct H :=
diff --git a/theories/Extraction/Readback.v b/theories/Extraction/Readback.v
index e9e5df0..4eb8b53 100644
--- a/theories/Extraction/Readback.v
+++ b/theories/Extraction/Readback.v
@@ -19,7 +19,7 @@ Inductive read_nf_order : nat -> domain_nf -> Prop :=
      read_nf_order s d{{{ ⇓ ℕ (succ m) }}} )
 | rnf_nat_neut :
   `( read_ne_order s m ->
-     read_nf_order s d{{{ ⇓ ℕ (⇑ ℕ m) }}} )
+     read_nf_order s d{{{ ⇓ ℕ (⇑ a m) }}} )
 | rnf_fn :
   `( read_typ_order s a ->
      eval_app_order m d{{{ ⇑! a s }}} ->
@@ -119,7 +119,7 @@ Equations read_nf_impl s d (H : read_nf_order s d) : { m | {{ Rnf d in s ↘ m }
 | s, d{{{ ⇓ ℕ (succ m) }}} , H =>
     let (M, HM) := read_nf_impl s d{{{ ⇓ ℕ m }}} _ in
     exist _ n{{{ succ M }}} _
-| s, d{{{ ⇓ ℕ (⇑ ℕ m) }}}  , H =>
+| s, d{{{ ⇓ ℕ (⇑ ^_ m) }}}  , H =>
     let (M, HM) := read_ne_impl s m _ in
     exist _ n{{{ ⇑ M }}} _
 | s, d{{{ ⇓ (Π a p B) m }}}, H =>