From 3bfedb1cdaa96d4fb4e56b7aaff4de34d474cd73 Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Wed, 8 May 2024 15:40:42 -0400
Subject: [PATCH] Refactor the module structure (#66)

* Refactor module structure for easier import

* Hide a meaningless warning
---
 theories/Core/Base.v                          |   8 +-
 theories/Core/Semantic/Domain.v               |  53 ++--
 theories/Core/Semantic/Evaluation.v           |  83 +----
 .../Core/Semantic/EvaluationDefinitions.v     |  81 +++++
 theories/Core/Semantic/EvaluationLemmas.v     |   3 +-
 theories/Core/Semantic/PER.v                  | 242 +-------------
 theories/Core/Semantic/PERDefinitions.v       | 243 +++++++++++++++
 theories/Core/Semantic/PERLemmas.v            |  15 +-
 theories/Core/Semantic/Readback.v             |  84 +----
 theories/Core/Semantic/ReadbackDefinitions.v  |  85 +++++
 theories/Core/Semantic/ReadbackLemmas.v       |   3 +-
 theories/Core/Semantic/Realizability.v        |   4 +-
 theories/Core/Syntactic/CtxEquiv.v            |   3 +-
 theories/Core/Syntactic/Presup.v              |   3 +-
 theories/Core/Syntactic/Relations.v           |   3 +-
 theories/Core/Syntactic/Syntax.v              | 100 +++---
 theories/Core/Syntactic/System.v              | 295 +-----------------
 theories/Core/Syntactic/SystemDefinitions.v   | 295 ++++++++++++++++++
 theories/Core/Syntactic/SystemLemmas.v        |   3 +-
 theories/_CoqProject                          |   6 +-
 20 files changed, 825 insertions(+), 787 deletions(-)
 create mode 100644 theories/Core/Semantic/EvaluationDefinitions.v
 create mode 100644 theories/Core/Semantic/PERDefinitions.v
 create mode 100644 theories/Core/Semantic/ReadbackDefinitions.v
 create mode 100644 theories/Core/Syntactic/SystemDefinitions.v

diff --git a/theories/Core/Base.v b/theories/Core/Base.v
index b0de8da4..ce40c126 100644
--- a/theories/Core/Base.v
+++ b/theories/Core/Base.v
@@ -1,7 +1,7 @@
-#[global] Declare Scope exp_scope.
-#[global] Delimit Scope exp_scope with exp.
-
-#[global] Bind Scope exp_scope with Sortclass.
+#[global] Declare Scope mcltt_scope.
+#[global] Delimit Scope mcltt_scope with mcltt.
+#[global] Bind Scope mcltt_scope with Sortclass.
 
 #[global] Declare Custom Entry judg.
+
 Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").
diff --git a/theories/Core/Semantic/Domain.v b/theories/Core/Semantic/Domain.v
index 4abd670f..3b7679f3 100644
--- a/theories/Core/Semantic/Domain.v
+++ b/theories/Core/Semantic/Domain.v
@@ -1,4 +1,4 @@
-From Mcltt Require Import Syntax.
+From Mcltt Require Export Syntax.
 
 Reserved Notation "'env'".
 
@@ -22,34 +22,39 @@ with domain_nf : Set :=
 | d_dom : domain -> domain -> domain_nf
 where "'env'" := (nat -> domain).
 
-#[global] Declare Custom Entry domain.
-#[global] Bind Scope exp_scope with domain.
-
-Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{'  x  '}}}'") : exp_scope.
-Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : exp_scope.
-Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : exp_scope.
-Notation "x" := x (in custom domain at level 0, x global) : exp_scope.
-Notation "'λ' p M" := (d_fn p M) (in custom domain at level 0, p custom domain at level 30, M custom exp at level 30) : exp_scope.
-Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : exp_scope.
-Notation "'ℕ'" := d_nat (in custom domain) : exp_scope.
-Notation "'𝕌' @ n" := (d_univ n) (in custom domain at level 0, n constr at level 0) : exp_scope.
-Notation "'Π' a p B" := (d_pi a p B) (in custom domain at level 0, a custom domain at level 30, p custom domain at level 0, B custom exp at level 30) : exp_scope.
-Notation "'zero'" := d_zero (in custom domain at level 0) : exp_scope.
-Notation "'succ' m" := (d_succ m) (in custom domain at level 30, m custom domain at level 30) : exp_scope.
-Notation "'rec' m 'under' p 'return' P | 'zero' -> mz | 'succ' -> MS 'end'" := (d_natrec p P mz MS m) (in custom domain at level 0, P custom exp at level 60, mz custom domain at level 60, MS custom exp at level 60, p custom domain at level 60, m custom domain at level 60) : exp_scope.
-Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : exp_scope.
-Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : exp_scope.
-Notation "'⇓' a m" := (d_dom a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : exp_scope.
-Notation "'⇑!' a n" := (d_neut a (d_var n)) (in custom domain at level 0, a custom domain at level 30, n constr at level 0) : exp_scope.
-
-Definition empty_env : env := fun x => d{{{ zero }}}.
+Definition empty_env : env := fun x => d_zero.
 Definition extend_env (p : env) (d : domain) : env :=
   fun n =>
     match n with
     | 0 => d
     | S n' => p n'
     end.
-Notation "p ↦ m" := (extend_env p m) (in custom domain at level 20, left associativity) : exp_scope.
 
 Definition drop_env (p : env) : env := fun n => p (S n).
-Notation "p '↯'" := (drop_env p) (in custom domain at level 10, p custom domain) : exp_scope.
+
+#[global] Declare Custom Entry domain.
+#[global] Bind Scope mcltt_scope with domain.
+
+Module Domain_Notations.
+  Export Syntax_Notations.
+
+  Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{'  x  '}}}'") : mcltt_scope.
+  Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : mcltt_scope.
+  Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : mcltt_scope.
+  Notation "x" := x (in custom domain at level 0, x global) : mcltt_scope.
+  Notation "'λ' p M" := (d_fn p M) (in custom domain at level 0, p custom domain at level 30, M custom exp at level 30) : mcltt_scope.
+  Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : mcltt_scope.
+  Notation "'ℕ'" := d_nat (in custom domain) : mcltt_scope.
+  Notation "'𝕌' @ n" := (d_univ n) (in custom domain at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'Π' a p B" := (d_pi a p B) (in custom domain at level 0, a custom domain at level 30, p custom domain at level 0, B custom exp at level 30) : mcltt_scope.
+  Notation "'zero'" := d_zero (in custom domain at level 0) : mcltt_scope.
+  Notation "'succ' m" := (d_succ m) (in custom domain at level 30, m custom domain at level 30) : mcltt_scope.
+  Notation "'rec' m 'under' p 'return' P | 'zero' -> mz | 'succ' -> MS 'end'" := (d_natrec p P mz MS m) (in custom domain at level 0, P custom exp at level 60, mz custom domain at level 60, MS custom exp at level 60, p custom domain at level 60, m custom domain at level 60) : mcltt_scope.
+  Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mcltt_scope.
+  Notation "'⇓' a m" := (d_dom a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mcltt_scope.
+  Notation "'⇑!' a n" := (d_neut a (d_var n)) (in custom domain at level 0, a custom domain at level 30, n constr at level 0) : mcltt_scope.
+
+  Notation "p ↦ m" := (extend_env p m) (in custom domain at level 20, left associativity) : mcltt_scope.
+  Notation "p '↯'" := (drop_env p) (in custom domain at level 10, p custom domain) : mcltt_scope.
+End Domain_Notations.
diff --git a/theories/Core/Semantic/Evaluation.v b/theories/Core/Semantic/Evaluation.v
index ef8acfe1..bbe67f65 100644
--- a/theories/Core/Semantic/Evaluation.v
+++ b/theories/Core/Semantic/Evaluation.v
@@ -1,82 +1 @@
-From Mcltt Require Import Base.
-From Mcltt Require Import Domain.
-From Mcltt Require Import Syntax.
-From Mcltt Require Import System.
-
-Reserved Notation "'⟦' M '⟧' p '↘' r" (in custom judg at level 80, M custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
-Reserved Notation "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" (in custom judg at level 80, m custom domain at level 99, A custom exp at level 99, MZ custom exp at level 99, MS custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
-Reserved Notation "'$|' m '&' n '|↘' r" (in custom judg at level 80, m custom domain at level 99, n custom domain at level 99, r custom domain at level 99).
-Reserved Notation "'⟦' σ '⟧s' p '↘' p'" (in custom judg at level 80, σ custom exp at level 99, p custom domain at level 99, p' custom domain at level 99).
-
-Generalizable All Variables.
-
-Inductive eval_exp : exp -> env -> domain -> Prop :=
-| eval_exp_typ :
-  `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
-| eval_exp_nat :
-  `( {{ ⟦ ℕ ⟧ p ↘ ℕ }} )
-| eval_exp_zero :
-  `( {{ ⟦ zero ⟧ p ↘ zero }} )
-| eval_exp_succ :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ ⟦ succ M ⟧ p ↘ succ m }} )
-| eval_exp_natrec :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
-     {{ ⟦ rec M return A | zero -> MZ | succ -> MS end ⟧ p ↘ r }} )
-| eval_exp_pi :
-  `( {{ ⟦ A ⟧ p ↘ a }} ->
-     {{ ⟦ Π A B ⟧ p ↘ Π a p B }} )
-| eval_exp_fn :
-  `( {{ ⟦ λ A M ⟧ p ↘ λ p M }} )
-| eval_exp_app :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ ⟦ N ⟧ p ↘ n }} ->
-     {{ $| m & n |↘ r }} ->
-     {{ ⟦ M N ⟧ p ↘ r }} )
-| eval_exp_sub :
-  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
-     {{ ⟦ M ⟧ p' ↘ m }} ->
-     {{ ⟦ M[σ] ⟧ p ↘ m }} )
-where "'⟦' e '⟧' p '↘' r" := (eval_exp e p r) (in custom judg)
-with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
-| eval_natrec_zero :
-  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
-     {{ rec zero ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ mz }} )
-| eval_natrec_succ :
-  `( {{ rec b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
-     {{ ⟦ MS ⟧ p ↦ b ↦ r ↘ ms }} ->
-     {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ms }} )
-| eval_natrec_neut :
-  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
-     {{ ⟦ A ⟧ p ↦ ⇑ ℕ m ↘ a }} ->
-     {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
-where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" := (eval_natrec A MZ MS m p r) (in custom judg)
-with eval_app : domain -> domain -> domain -> Prop :=
-| eval_app_fn :
-  `( {{ ⟦ M ⟧ p ↦ n ↘ m }} ->
-     {{ $| λ p M & n |↘ m }} )
-| eval_app_neut :
-  `( {{ ⟦ B ⟧ p ↦ n ↘ b }} ->
-     {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a n)) }} )
-where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
-with eval_sub : sub -> env -> env -> Prop :=
-| eval_sub_id :
-  `( {{ ⟦ Id ⟧s p ↘ p }} )
-| eval_sub_weaken :
-  `( {{ ⟦ Wk ⟧s p ↘ p↯ }} )
-| eval_sub_extend :
-  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
-     {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ ⟦ σ ,, M ⟧s p ↘ p' ↦ m }} )
-| eval_sub_compose :
-  `( {{ ⟦ τ ⟧s p ↘ p' }} ->
-     {{ ⟦ σ ⟧s p' ↘ p'' }} ->
-     {{ ⟦ σ ∘ τ ⟧s p ↘ p'' }} )
-where "'⟦' σ '⟧s' p '↘' p'" := (eval_sub σ p p') (in custom judg)
-.
-
-Scheme eval_exp_mut_ind := Induction for eval_exp Sort Prop
-with eval_natrec_mut_ind := Induction for eval_natrec Sort Prop
-with eval_app_mut_ind := Induction for eval_app Sort Prop
-with eval_sub_mut_ind := Induction for eval_sub Sort Prop.
+From Mcltt Require Export EvaluationDefinitions EvaluationLemmas.
diff --git a/theories/Core/Semantic/EvaluationDefinitions.v b/theories/Core/Semantic/EvaluationDefinitions.v
new file mode 100644
index 00000000..84a4c68d
--- /dev/null
+++ b/theories/Core/Semantic/EvaluationDefinitions.v
@@ -0,0 +1,81 @@
+From Mcltt Require Import Base.
+From Mcltt Require Export Domain.
+Import Domain_Notations.
+
+Reserved Notation "'⟦' M '⟧' p '↘' r" (in custom judg at level 80, M custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" (in custom judg at level 80, m custom domain at level 99, A custom exp at level 99, MZ custom exp at level 99, MS custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'$|' m '&' n '|↘' r" (in custom judg at level 80, m custom domain at level 99, n custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'⟦' σ '⟧s' p '↘' p'" (in custom judg at level 80, σ custom exp at level 99, p custom domain at level 99, p' custom domain at level 99).
+
+Generalizable All Variables.
+
+Inductive eval_exp : exp -> env -> domain -> Prop :=
+| eval_exp_typ :
+  `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
+| eval_exp_nat :
+  `( {{ ⟦ ℕ ⟧ p ↘ ℕ }} )
+| eval_exp_zero :
+  `( {{ ⟦ zero ⟧ p ↘ zero }} )
+| eval_exp_succ :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ succ M ⟧ p ↘ succ m }} )
+| eval_exp_natrec :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     {{ ⟦ rec M return A | zero -> MZ | succ -> MS end ⟧ p ↘ r }} )
+| eval_exp_pi :
+  `( {{ ⟦ A ⟧ p ↘ a }} ->
+     {{ ⟦ Π A B ⟧ p ↘ Π a p B }} )
+| eval_exp_fn :
+  `( {{ ⟦ λ A M ⟧ p ↘ λ p M }} )
+| eval_exp_app :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ N ⟧ p ↘ n }} ->
+     {{ $| m & n |↘ r }} ->
+     {{ ⟦ M N ⟧ p ↘ r }} )
+| eval_exp_sub :
+  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
+     {{ ⟦ M ⟧ p' ↘ m }} ->
+     {{ ⟦ M[σ] ⟧ p ↘ m }} )
+where "'⟦' e '⟧' p '↘' r" := (eval_exp e p r) (in custom judg)
+with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
+| eval_natrec_zero :
+  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
+     {{ rec zero ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ mz }} )
+| eval_natrec_succ :
+  `( {{ rec b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     {{ ⟦ MS ⟧ p ↦ b ↦ r ↘ ms }} ->
+     {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ms }} )
+| eval_natrec_neut :
+  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
+     {{ ⟦ A ⟧ p ↦ ⇑ ℕ m ↘ a }} ->
+     {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
+where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" := (eval_natrec A MZ MS m p r) (in custom judg)
+with eval_app : domain -> domain -> domain -> Prop :=
+| eval_app_fn :
+  `( {{ ⟦ M ⟧ p ↦ n ↘ m }} ->
+     {{ $| λ p M & n |↘ m }} )
+| eval_app_neut :
+  `( {{ ⟦ B ⟧ p ↦ n ↘ b }} ->
+     {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a n)) }} )
+where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
+with eval_sub : sub -> env -> env -> Prop :=
+| eval_sub_id :
+  `( {{ ⟦ Id ⟧s p ↘ p }} )
+| eval_sub_weaken :
+  `( {{ ⟦ Wk ⟧s p ↘ p↯ }} )
+| eval_sub_extend :
+  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
+     {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ σ ,, M ⟧s p ↘ p' ↦ m }} )
+| eval_sub_compose :
+  `( {{ ⟦ τ ⟧s p ↘ p' }} ->
+     {{ ⟦ σ ⟧s p' ↘ p'' }} ->
+     {{ ⟦ σ ∘ τ ⟧s p ↘ p'' }} )
+where "'⟦' σ '⟧s' p '↘' p'" := (eval_sub σ p p') (in custom judg)
+.
+
+Scheme eval_exp_mut_ind := Induction for eval_exp Sort Prop
+with eval_natrec_mut_ind := Induction for eval_natrec Sort Prop
+with eval_app_mut_ind := Induction for eval_app Sort Prop
+with eval_sub_mut_ind := Induction for eval_sub Sort Prop.
diff --git a/theories/Core/Semantic/EvaluationLemmas.v b/theories/Core/Semantic/EvaluationLemmas.v
index 5f35068f..00ee3b27 100644
--- a/theories/Core/Semantic/EvaluationLemmas.v
+++ b/theories/Core/Semantic/EvaluationLemmas.v
@@ -1,5 +1,6 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base Domain Evaluation LibTactics Syntax System.
+From Mcltt Require Import Base LibTactics EvaluationDefinitions.
+Import Domain_Notations.
 
 Section functional_eval.
   Let functional_eval_exp_prop M p m1 (_ : {{ ⟦ M ⟧ p ↘ m1 }}) : Prop := forall m2 (Heval2: {{ ⟦ M ⟧ p ↘ m2 }}), m1 = m2.
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index 47519369..e749f9a8 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -1,241 +1 @@
-From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
-From Equations Require Import Equations.
-From Mcltt Require Import Base Domain Evaluation LibTactics Readback Syntax System.
-
-Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr).
-Notation "'DF' a ≈ b ∈ R ↘ R'" := ((R a b R' : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr, R' constr).
-Notation "'Exp' a ≈ b ∈ R" := (R a b : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr).
-Notation "'EF' a ≈ b ∈ R ↘ R'" := (R a b R' : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr, R' constr).
-
-Generalizable All Variables.
-
-(** Helper Bundles *)
-Inductive rel_mod_eval (R : domain -> domain -> relation domain -> Prop) A p A' p' R' : Prop := mk_rel_mod_eval : forall a a', {{ ⟦ A ⟧ p ↘ a }} -> {{ ⟦ A' ⟧ p' ↘ a' }} -> {{ DF a ≈ a' ∈ R ↘ R' }} -> rel_mod_eval R A p A' p' R'.
-#[global]
-Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
-
-Inductive rel_mod_app (R : relation domain) f a f' a' : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app R f a f' a'.
-#[global]
-Arguments mk_rel_mod_app {_ _ _ _ _}.
-
-Ltac destruct_rel_by_assumption in_rel H :=
-  repeat
-    match goal with
-    | H' : {{ Dom ~?c ≈ ~?c' ∈ ?in_rel0 }} |- _ =>
-        tryif (unify in_rel0 in_rel)
-        then (destruct (H _ _ H') as []; destruct_all; mark_with H' 1)
-        else fail
-    end;
-  unmark_all_with 1.
-Ltac destruct_rel_mod_eval :=
-  repeat
-    match goal with
-    | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_eval _ _ _ _ _ _) |- _ =>
-        destruct_rel_by_assumption in_rel H; mark H
-    end;
-  unmark_all.
-Ltac destruct_rel_mod_app :=
-  repeat
-    match goal with
-    | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_app _ _ _ _ _) |- _ =>
-        destruct_rel_by_assumption in_rel H; mark H
-    end;
-  unmark_all.
-
-(** (Some Elements of) PER Lattice *)
-
-Definition per_bot : relation domain_ne := fun m n => (forall s, exists L, {{ Rne m in s ↘ L }} /\ {{ Rne n in s ↘ L }}).
-#[global]
-Arguments per_bot /.
-
-Definition per_top : relation domain_nf := fun m n => (forall s, exists L, {{ Rnf m in s ↘ L }} /\ {{ Rnf n in s ↘ L }}).
-#[global]
-Arguments per_top /.
-
-Definition per_top_typ : relation domain := fun a b => (forall s, exists C, {{ Rtyp a in s ↘ C }} /\ {{ Rtyp b in s ↘ C }}).
-#[global]
-Arguments per_top_typ /.
-
-Inductive per_nat : relation domain :=
-| per_nat_zero : {{ Dom zero ≈ zero ∈ per_nat }}
-| per_nat_succ :
-  `{ {{ Dom m ≈ n ∈ per_nat }} ->
-     {{ Dom succ m ≈ succ n ∈ per_nat }} }
-| per_nat_neut :
-  `{ {{ Dom m ≈ n ∈ per_bot }} ->
-     {{ Dom ⇑ ℕ m ≈ ⇑ ℕ n ∈ per_nat }} }
-.
-
-Inductive per_ne : relation domain :=
-| per_ne_neut :
-  `{ {{ Dom m ≈ m' ∈ per_bot }} ->
-     {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ per_ne }} }
-.
-
-(** Universe/Element PER Definition *)
-
-Section Per_univ_elem_core_def.
-  Variable (i : nat) (per_univ_rec : forall {j}, j < i -> relation domain).
-
-  Inductive per_univ_elem_core : domain -> domain -> relation domain -> Prop :=
-  | per_univ_elem_core_univ :
-    `{ forall (lt_j_i : j < i),
-          j = j' ->
-          {{ DF 𝕌@j ≈ 𝕌@j' ∈ per_univ_elem_core ↘ per_univ_rec lt_j_i }} }
-  | per_univ_elem_core_nat : {{ DF ℕ ≈ ℕ ∈ per_univ_elem_core ↘ per_nat }}
-  | per_univ_elem_core_pi :
-    `{ forall (in_rel : relation domain)
-         (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
-         (equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel}}),
-          PER in_rel ->
-          (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
-              rel_mod_eval per_univ_elem_core B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
-          (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
-          {{ DF Π a p B ≈ Π a' p' B' ∈ per_univ_elem_core ↘ elem_rel }} }
-  | per_univ_elem_core_neut :
-    `{ {{ Dom b ≈ b' ∈ per_bot }} ->
-       {{ DF ⇑ a b ≈ ⇑ a' b' ∈ per_univ_elem_core ↘ per_ne }} }
-  .
-
-  Hypothesis
-    (motive : domain -> domain -> relation domain -> Prop).
-
-  Hypothesis
-    (case_U : forall (j j' : nat) (lt_j_i : j < i), j = j' -> motive d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ_rec lt_j_i)).
-
-  Hypothesis
-    (case_nat : motive d{{{ ℕ }}} d{{{ ℕ }}} per_nat).
-
-  Hypothesis
-    (case_Pi :
-      forall {A p B A' p' B' in_rel elem_rel}
-        (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
-        {{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} ->
-        motive A A' in_rel ->
-        PER in_rel ->
-        (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
-            rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
-        (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
-        motive d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel).
-
-  Hypothesis
-    (case_ne : (forall {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)).
-
-  #[derive(equations=no, eliminator=no)]
-  Equations per_univ_elem_core_strong_ind a b R (H : {{ DF a ≈ b ∈ per_univ_elem_core ↘ R }}) : {{ DF a ≈ b ∈ motive ↘ R }} :=
-  | a, b, R, (per_univ_elem_core_univ lt_j_i eq)                         => case_U _ _ lt_j_i eq;
-  | a, b, R, per_univ_elem_core_nat                                      => case_nat;
-  | a, b, R, (per_univ_elem_core_pi in_rel out_rel equiv_a_a' per HT HE) =>
-      case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a') per
-        (fun _ _ equiv_c_c' => match HT _ _ equiv_c_c' with
-                              | mk_rel_mod_eval b b' evb evb' Rel =>
-                                  mk_rel_mod_eval b b' evb evb' (conj _ (per_univ_elem_core_strong_ind _ _ _ Rel))
-                              end)
-        HE;
-  | a, b, R, (per_univ_elem_core_neut equiv_b_b')                        => case_ne equiv_b_b'.
-
-End Per_univ_elem_core_def.
-
-Global Hint Constructors per_univ_elem_core : mcltt.
-
-Equations per_univ_elem (i : nat) : domain -> domain -> relation domain -> Prop by wf i :=
-| i => per_univ_elem_core i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}).
-
-Definition per_univ (i : nat) : relation domain := fun a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem i ↘ R' }}.
-#[global]
-Arguments per_univ _ _ _ /.
-
-Lemma per_univ_elem_core_univ' : forall j i,
-    j < i ->
-    {{ DF 𝕌@j ≈ 𝕌@j ∈ per_univ_elem i ↘ per_univ j }}.
-Proof.
-  intros.
-  simp per_univ_elem.
-
-  eapply (per_univ_elem_core_univ i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}) H).
-  reflexivity.
-Qed.
-Global Hint Resolve per_univ_elem_core_univ' : mcltt.
-
-(** Universe/Element PER Induction Principle *)
-
-Section Per_univ_elem_ind_def.
-  Hypothesis
-    (motive : nat -> domain -> domain -> relation domain -> Prop).
-
-  Hypothesis
-    (case_U : forall j j' i, j < i -> j = j' ->
-                        (forall A B R, {{ DF A ≈ B ∈ per_univ_elem j ↘ R }} -> motive j A B R) ->
-                        motive i d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ j)).
-
-  Hypothesis
-    (case_N : forall i, motive i d{{{ ℕ }}} d{{{ ℕ }}} per_nat).
-
-  Hypothesis
-    (case_Pi :
-      forall i {A p B A' p' B' in_rel elem_rel}
-        (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
-        {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} ->
-        motive i A A' in_rel ->
-        PER in_rel ->
-        (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
-            rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
-        (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
-        motive i d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel).
-
-  Hypothesis
-    (case_ne : (forall i {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive i d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)).
-
-  #[local]
-  Ltac def_simp := simp per_univ_elem in *.
-
-  #[derive(equations=no, eliminator=no), tactic="def_simp"]
-  Equations per_univ_elem_ind' (i : nat) (a b : domain) (R : relation domain)
-    (H : {{ DF a ≈ b ∈ per_univ_elem_core i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}) ↘ R }}) : {{ DF a ≈ b ∈ motive i ↘ R }} by wf i :=
-  | i, a, b, R, H =>
-      per_univ_elem_core_strong_ind i _ (motive i)
-        (fun j j' j_lt_i eq => case_U j j' i j_lt_i eq (fun A B R' H' => per_univ_elem_ind' _ A B R' _))
-        (case_N i)
-        (fun A p B A' p' B' in_rel elem_rel out_rel HA IHA per HT HE => case_Pi i out_rel _ IHA per _ HE)
-        (@case_ne i)
-        a b R H.
-
-  #[derive(equations=no, eliminator=no), tactic="def_simp"]
-  Equations per_univ_elem_ind i a b R (H : per_univ_elem i a b R) : motive i a b R :=
-  | i, a, b, R, H := per_univ_elem_ind' i a b R _.
-
-End Per_univ_elem_ind_def.
-
-(** Universe/Element PER Helper Tactics *)
-
-Ltac invert_per_univ_elem H :=
-  simp per_univ_elem in H;
-  inversion H;
-  subst;
-  try rewrite <- per_univ_elem_equation_1 in *.
-
-Ltac per_univ_elem_econstructor :=
-  simp per_univ_elem;
-  econstructor;
-  try rewrite <- per_univ_elem_equation_1 in *.
-
-(** Context/Environment PER *)
-
-Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
-
-Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
-| per_ctx_env_nil :
-  `{ (Env = fun p p' => True) ->
-     {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ Env }} }
-| per_ctx_env_cons :
-  `{ forall (tail_rel : relation env)
-        (head_rel : forall {p p'}, {{ Dom p ≈ p' ∈ tail_rel }} -> relation domain)
-        (equiv_Γ_Γ' : {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ tail_rel }}),
-        (forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), rel_typ i A p A' p' (head_rel equiv_p_p')) ->
-        (Env = fun p p' => exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel }}),
-                   {{ Dom ~(p 0) ≈ ~(p' 0) ∈ head_rel equiv_p_drop_p'_drop }}) ->
-        {{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ Env }} }
-.
-
-Definition per_ctx : relation ctx := fun Γ Γ' => exists R', per_ctx_env Γ Γ' R'.
-Definition valid_ctx : ctx -> Prop := fun Γ => per_ctx Γ Γ.
+From Mcltt Require Export PERDefinitions PERLemmas.
diff --git a/theories/Core/Semantic/PERDefinitions.v b/theories/Core/Semantic/PERDefinitions.v
new file mode 100644
index 00000000..e0ac8419
--- /dev/null
+++ b/theories/Core/Semantic/PERDefinitions.v
@@ -0,0 +1,243 @@
+From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
+From Equations Require Import Equations.
+From Mcltt Require Import Base Evaluation LibTactics Readback.
+From Mcltt Require Export Domain.
+Import Domain_Notations.
+
+Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr).
+Notation "'DF' a ≈ b ∈ R ↘ R'" := ((R a b R' : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr, R' constr).
+Notation "'Exp' a ≈ b ∈ R" := (R a b : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr).
+Notation "'EF' a ≈ b ∈ R ↘ R'" := (R a b R' : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr, R' constr).
+
+Generalizable All Variables.
+
+(** Helper Bundles *)
+Inductive rel_mod_eval (R : domain -> domain -> relation domain -> Prop) A p A' p' R' : Prop := mk_rel_mod_eval : forall a a', {{ ⟦ A ⟧ p ↘ a }} -> {{ ⟦ A' ⟧ p' ↘ a' }} -> {{ DF a ≈ a' ∈ R ↘ R' }} -> rel_mod_eval R A p A' p' R'.
+#[global]
+Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
+
+Inductive rel_mod_app (R : relation domain) f a f' a' : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app R f a f' a'.
+#[global]
+Arguments mk_rel_mod_app {_ _ _ _ _}.
+
+Ltac destruct_rel_by_assumption in_rel H :=
+  repeat
+    match goal with
+    | H' : {{ Dom ~?c ≈ ~?c' ∈ ?in_rel0 }} |- _ =>
+        tryif (unify in_rel0 in_rel)
+        then (destruct (H _ _ H') as []; destruct_all; mark_with H' 1)
+        else fail
+    end;
+  unmark_all_with 1.
+Ltac destruct_rel_mod_eval :=
+  repeat
+    match goal with
+    | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_eval _ _ _ _ _ _) |- _ =>
+        destruct_rel_by_assumption in_rel H; mark H
+    end;
+  unmark_all.
+Ltac destruct_rel_mod_app :=
+  repeat
+    match goal with
+    | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_app _ _ _ _ _) |- _ =>
+        destruct_rel_by_assumption in_rel H; mark H
+    end;
+  unmark_all.
+
+(** (Some Elements of) PER Lattice *)
+
+Definition per_bot : relation domain_ne := fun m n => (forall s, exists L, {{ Rne m in s ↘ L }} /\ {{ Rne n in s ↘ L }}).
+#[global]
+Arguments per_bot /.
+
+Definition per_top : relation domain_nf := fun m n => (forall s, exists L, {{ Rnf m in s ↘ L }} /\ {{ Rnf n in s ↘ L }}).
+#[global]
+Arguments per_top /.
+
+Definition per_top_typ : relation domain := fun a b => (forall s, exists C, {{ Rtyp a in s ↘ C }} /\ {{ Rtyp b in s ↘ C }}).
+#[global]
+Arguments per_top_typ /.
+
+Inductive per_nat : relation domain :=
+| per_nat_zero : {{ Dom zero ≈ zero ∈ per_nat }}
+| per_nat_succ :
+  `{ {{ Dom m ≈ n ∈ per_nat }} ->
+     {{ Dom succ m ≈ succ n ∈ per_nat }} }
+| per_nat_neut :
+  `{ {{ Dom m ≈ n ∈ per_bot }} ->
+     {{ Dom ⇑ ℕ m ≈ ⇑ ℕ n ∈ per_nat }} }
+.
+
+Inductive per_ne : relation domain :=
+| per_ne_neut :
+  `{ {{ Dom m ≈ m' ∈ per_bot }} ->
+     {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ per_ne }} }
+.
+
+(** Universe/Element PER Definition *)
+
+Section Per_univ_elem_core_def.
+  Variable (i : nat) (per_univ_rec : forall {j}, j < i -> relation domain).
+
+  Inductive per_univ_elem_core : domain -> domain -> relation domain -> Prop :=
+  | per_univ_elem_core_univ :
+    `{ forall (lt_j_i : j < i),
+          j = j' ->
+          {{ DF 𝕌@j ≈ 𝕌@j' ∈ per_univ_elem_core ↘ per_univ_rec lt_j_i }} }
+  | per_univ_elem_core_nat : {{ DF ℕ ≈ ℕ ∈ per_univ_elem_core ↘ per_nat }}
+  | per_univ_elem_core_pi :
+    `{ forall (in_rel : relation domain)
+         (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
+         (equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel}}),
+          PER in_rel ->
+          (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
+              rel_mod_eval per_univ_elem_core B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
+          (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
+          {{ DF Π a p B ≈ Π a' p' B' ∈ per_univ_elem_core ↘ elem_rel }} }
+  | per_univ_elem_core_neut :
+    `{ {{ Dom b ≈ b' ∈ per_bot }} ->
+       {{ DF ⇑ a b ≈ ⇑ a' b' ∈ per_univ_elem_core ↘ per_ne }} }
+  .
+
+  Hypothesis
+    (motive : domain -> domain -> relation domain -> Prop).
+
+  Hypothesis
+    (case_U : forall (j j' : nat) (lt_j_i : j < i), j = j' -> motive d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ_rec lt_j_i)).
+
+  Hypothesis
+    (case_nat : motive d{{{ ℕ }}} d{{{ ℕ }}} per_nat).
+
+  Hypothesis
+    (case_Pi :
+      forall {A p B A' p' B' in_rel elem_rel}
+        (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
+        {{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} ->
+        motive A A' in_rel ->
+        PER in_rel ->
+        (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
+            rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
+        (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
+        motive d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel).
+
+  Hypothesis
+    (case_ne : (forall {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)).
+
+  #[derive(equations=no, eliminator=no)]
+  Equations per_univ_elem_core_strong_ind a b R (H : {{ DF a ≈ b ∈ per_univ_elem_core ↘ R }}) : {{ DF a ≈ b ∈ motive ↘ R }} :=
+  | a, b, R, (per_univ_elem_core_univ lt_j_i eq)                         => case_U _ _ lt_j_i eq;
+  | a, b, R, per_univ_elem_core_nat                                      => case_nat;
+  | a, b, R, (per_univ_elem_core_pi in_rel out_rel equiv_a_a' per HT HE) =>
+      case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a') per
+        (fun _ _ equiv_c_c' => match HT _ _ equiv_c_c' with
+                              | mk_rel_mod_eval b b' evb evb' Rel =>
+                                  mk_rel_mod_eval b b' evb evb' (conj _ (per_univ_elem_core_strong_ind _ _ _ Rel))
+                              end)
+        HE;
+  | a, b, R, (per_univ_elem_core_neut equiv_b_b')                        => case_ne equiv_b_b'.
+
+End Per_univ_elem_core_def.
+
+Global Hint Constructors per_univ_elem_core : mcltt.
+
+Equations per_univ_elem (i : nat) : domain -> domain -> relation domain -> Prop by wf i :=
+| i => per_univ_elem_core i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}).
+
+Definition per_univ (i : nat) : relation domain := fun a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem i ↘ R' }}.
+#[global]
+Arguments per_univ _ _ _ /.
+
+Lemma per_univ_elem_core_univ' : forall j i,
+    j < i ->
+    {{ DF 𝕌@j ≈ 𝕌@j ∈ per_univ_elem i ↘ per_univ j }}.
+Proof.
+  intros.
+  simp per_univ_elem.
+
+  eapply (per_univ_elem_core_univ i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}) H).
+  reflexivity.
+Qed.
+Global Hint Resolve per_univ_elem_core_univ' : mcltt.
+
+(** Universe/Element PER Induction Principle *)
+
+Section Per_univ_elem_ind_def.
+  Hypothesis
+    (motive : nat -> domain -> domain -> relation domain -> Prop).
+
+  Hypothesis
+    (case_U : forall j j' i, j < i -> j = j' ->
+                        (forall A B R, {{ DF A ≈ B ∈ per_univ_elem j ↘ R }} -> motive j A B R) ->
+                        motive i d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ j)).
+
+  Hypothesis
+    (case_N : forall i, motive i d{{{ ℕ }}} d{{{ ℕ }}} per_nat).
+
+  Hypothesis
+    (case_Pi :
+      forall i {A p B A' p' B' in_rel elem_rel}
+        (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain),
+        {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} ->
+        motive i A A' in_rel ->
+        PER in_rel ->
+        (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
+            rel_mod_eval (fun x y R => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i x y R) B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
+        (forall f f', elem_rel f f' = forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app (out_rel equiv_c_c') f c f' c') ->
+        motive i d{{{ Π A p B }}} d{{{ Π A' p' B' }}} elem_rel).
+
+  Hypothesis
+    (case_ne : (forall i {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive i d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}} per_ne)).
+
+  #[local]
+  Ltac def_simp := simp per_univ_elem in *.
+
+  #[derive(equations=no, eliminator=no), tactic="def_simp"]
+  Equations per_univ_elem_ind' (i : nat) (a b : domain) (R : relation domain)
+    (H : {{ DF a ≈ b ∈ per_univ_elem_core i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}) ↘ R }}) : {{ DF a ≈ b ∈ motive i ↘ R }} by wf i :=
+  | i, a, b, R, H =>
+      per_univ_elem_core_strong_ind i _ (motive i)
+        (fun j j' j_lt_i eq => case_U j j' i j_lt_i eq (fun A B R' H' => per_univ_elem_ind' _ A B R' _))
+        (case_N i)
+        (fun A p B A' p' B' in_rel elem_rel out_rel HA IHA per HT HE => case_Pi i out_rel _ IHA per _ HE)
+        (@case_ne i)
+        a b R H.
+
+  #[derive(equations=no, eliminator=no), tactic="def_simp"]
+  Equations per_univ_elem_ind i a b R (H : per_univ_elem i a b R) : motive i a b R :=
+  | i, a, b, R, H := per_univ_elem_ind' i a b R _.
+
+End Per_univ_elem_ind_def.
+
+(** Universe/Element PER Helper Tactics *)
+
+Ltac invert_per_univ_elem H :=
+  simp per_univ_elem in H;
+  inversion H;
+  subst;
+  try rewrite <- per_univ_elem_equation_1 in *.
+
+Ltac per_univ_elem_econstructor :=
+  simp per_univ_elem;
+  econstructor;
+  try rewrite <- per_univ_elem_equation_1 in *.
+
+(** Context/Environment PER *)
+
+Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
+
+Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
+| per_ctx_env_nil :
+  `{ (Env = fun p p' => True) ->
+     {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ Env }} }
+| per_ctx_env_cons :
+  `{ forall (tail_rel : relation env)
+        (head_rel : forall {p p'}, {{ Dom p ≈ p' ∈ tail_rel }} -> relation domain)
+        (equiv_Γ_Γ' : {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ tail_rel }}),
+        (forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), rel_typ i A p A' p' (head_rel equiv_p_p')) ->
+        (Env = fun p p' => exists (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel }}),
+                   {{ Dom ~(p 0) ≈ ~(p' 0) ∈ head_rel equiv_p_drop_p'_drop }}) ->
+        {{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ Env }} }
+.
+
+Definition per_ctx : relation ctx := fun Γ Γ' => exists R', per_ctx_env Γ Γ' R'.
+Definition valid_ctx : ctx -> Prop := fun Γ => per_ctx Γ Γ.
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index 35102bd5..06a08a92 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -1,5 +1,6 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
-From Mcltt Require Import Axioms Base Domain Evaluation EvaluationLemmas LibTactics PER Readback ReadbackLemmas Syntax System.
+From Mcltt Require Import Axioms Base Evaluation LibTactics PERDefinitions Readback.
+Import Domain_Notations.
 
 (* Lemma rel_mod_eval_ex_pull : *)
 (*   forall (A : Type) (P : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R, *)
@@ -97,6 +98,18 @@ Qed.
 #[export]
 Hint Resolve per_top_trans : mcltt.
 
+Lemma per_bot_then_per_top : forall m m' a a' b b' c c',
+    {{ Dom m ≈ m' ∈ per_bot }} ->
+    {{ Dom ⇓ (⇑ a b) ⇑ c m ≈ ⇓ (⇑ a' b') ⇑ c' m' ∈ per_top }}.
+Proof.
+  intros * H s.
+  specialize (H s) as [? []].
+  eexists; split; constructor; eassumption.
+Qed.
+
+#[export]
+Hint Resolve per_bot_then_per_top : mcltt.
+
 Lemma per_top_typ_sym : forall m n,
     {{ Dom m ≈ n ∈ per_top_typ }} ->
     {{ Dom n ≈ m ∈ per_top_typ }}.
diff --git a/theories/Core/Semantic/Readback.v b/theories/Core/Semantic/Readback.v
index ddd839ae..9a282331 100644
--- a/theories/Core/Semantic/Readback.v
+++ b/theories/Core/Semantic/Readback.v
@@ -1,83 +1 @@
-From Mcltt Require Import Base Domain Evaluation Syntax System.
-
-Reserved Notation "'Rnf' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
-Reserved Notation "'Rne' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
-Reserved Notation "'Rtyp' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
-
-Generalizable All Variables.
-
-Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
-| read_nf_type :
-  `( {{ Rtyp a in s ↘ A }} ->
-     {{ Rnf ⇓ 𝕌@i a in s ↘ A }} )
-| read_nf_zero :
-  `( {{ Rnf ⇓ ℕ zero in s ↘ zero }} )
-| read_nf_succ :
-  `( {{ Rnf ⇓ ℕ m in s ↘ M }} ->
-     {{ Rnf ⇓ ℕ (succ m) in s ↘ succ M }} )
-| read_nf_nat_neut :
-  `( {{ Rne m in s ↘ M }} ->
-     {{ Rnf ⇓ ℕ (⇑ ℕ m) in s ↘ ⇑ M }} )
-| read_nf_fn :
-  (* Nf of arg type *)
-  `( {{ Rtyp a in s ↘ A }} ->
-
-     (* Nf of eta-expanded body *)
-     {{ $| m & ⇑! a s |↘ m' }} ->
-     {{ ⟦ B ⟧ p ↦ ⇑! a s ↘ b }} ->
-     {{ Rnf ⇓ b m' in S s ↘ M }} ->
-
-     {{ Rnf ⇓ (Π a p B) m in s ↘ λ A M }} )
-| read_nf_neut :
-  `( {{ Rne m in s ↘ M }} ->
-     {{ Rnf ⇓ (⇑ a b) (⇑ c m) in s ↘ ⇑ M }} )
-where "'Rnf' m 'in' s ↘ M" := (read_nf s m M) (in custom judg) : exp_scope
-with read_ne : nat -> domain_ne -> ne -> Prop :=
-| read_ne_var :
-  `( {{ Rne !x in s ↘ #(s - x - 1) }} )
-| read_ne_app :
-  `( {{ Rne m in s ↘ M }} ->
-     {{ Rnf n in s ↘ N }} ->
-     {{ Rne m n in s ↘ M N }} )
-| read_ne_natrec :
-  (* Nf of motive *)
-  `( {{ ⟦ B ⟧ p ↦ ⇑! ℕ s ↘ b }} ->
-     {{ Rtyp b in S s ↘ B' }} ->
-
-     (* Nf of mz *)
-     {{ ⟦ B ⟧ p ↦ zero ↘ bz }} ->
-     {{ Rnf ⇓ bz mz in s ↘ MZ }} ->
-
-     (* Nf of MS *)
-     {{ ⟦ B ⟧ p ↦ succ (⇑! ℕ s) ↘ bs }} ->
-     {{ ⟦ MS ⟧ p ↦ ⇑! ℕ s ↦ ⇑! b (S s) ↘ ms }} ->
-     {{ Rnf ⇓ bs ms in S (S s) ↘ MS' }} ->
-
-     (* Ne of m *)
-     {{ Rne m in s ↘ M }} ->
-
-     {{ Rne rec m under p return B | zero -> mz | succ -> MS end in s ↘ rec M return B' | zero -> MZ | succ -> MS' end }} )
-where "'Rne' m 'in' s ↘ M" := (read_ne s m M) (in custom judg) : exp_scope
-with read_typ : nat -> domain -> nf -> Prop :=
-| read_typ_univ :
-  `( {{ Rtyp 𝕌@i in s ↘ Type@i }} )
-| read_typ_nat :
-  `( {{ Rtyp ℕ in s ↘ ℕ }} )
-| read_typ_pi :
-  (* Nf of arg type *)
-  `( {{ Rtyp a in s ↘ A }} ->
-
-     (* Nf of ret type *)
-     {{ ⟦ B ⟧ p ↦ ⇑! a s ↘ b }} ->
-     {{ Rtyp b in S s ↘ B' }} ->
-
-     {{ Rtyp Π a p B in s ↘ Π A B' }})
-| read_typ_neut :
-  `( {{ Rne b in s ↘ B }} ->
-     {{ Rtyp ⇑ a b in s ↘ ⇑ B }})
-where "'Rtyp' m 'in' s ↘ M" := (read_typ s m M) (in custom judg) : exp_scope
-.
-
-Scheme read_nf_mut_ind := Induction for read_nf Sort Prop
-with read_ne_mut_ind := Induction for read_ne Sort Prop
-with read_typ_mut_ind := Induction for read_typ Sort Prop.
+From Mcltt Require Export ReadbackDefinitions ReadbackLemmas.
diff --git a/theories/Core/Semantic/ReadbackDefinitions.v b/theories/Core/Semantic/ReadbackDefinitions.v
new file mode 100644
index 00000000..ba94c3e0
--- /dev/null
+++ b/theories/Core/Semantic/ReadbackDefinitions.v
@@ -0,0 +1,85 @@
+From Mcltt Require Import Base Evaluation.
+From Mcltt Require Export Domain.
+Import Domain_Notations.
+
+Reserved Notation "'Rnf' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
+Reserved Notation "'Rne' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
+Reserved Notation "'Rtyp' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).
+
+Generalizable All Variables.
+
+Inductive read_nf : nat -> domain_nf -> nf -> Prop :=
+| read_nf_type :
+  `( {{ Rtyp a in s ↘ A }} ->
+     {{ Rnf ⇓ 𝕌@i a in s ↘ A }} )
+| read_nf_zero :
+  `( {{ Rnf ⇓ ℕ zero in s ↘ zero }} )
+| read_nf_succ :
+  `( {{ Rnf ⇓ ℕ m in s ↘ M }} ->
+     {{ Rnf ⇓ ℕ (succ m) in s ↘ succ M }} )
+| read_nf_nat_neut :
+  `( {{ Rne m in s ↘ M }} ->
+     {{ Rnf ⇓ ℕ (⇑ ℕ m) in s ↘ ⇑ M }} )
+| read_nf_fn :
+  (* Nf of arg type *)
+  `( {{ Rtyp a in s ↘ A }} ->
+
+     (* Nf of eta-expanded body *)
+     {{ $| m & ⇑! a s |↘ m' }} ->
+     {{ ⟦ B ⟧ p ↦ ⇑! a s ↘ b }} ->
+     {{ Rnf ⇓ b m' in S s ↘ M }} ->
+
+     {{ Rnf ⇓ (Π a p B) m in s ↘ λ A M }} )
+| read_nf_neut :
+  `( {{ Rne m in s ↘ M }} ->
+     {{ Rnf ⇓ (⇑ a b) (⇑ c m) in s ↘ ⇑ M }} )
+where "'Rnf' m 'in' s ↘ M" := (read_nf s m M) (in custom judg) : type_scope
+with read_ne : nat -> domain_ne -> ne -> Prop :=
+| read_ne_var :
+  `( {{ Rne !x in s ↘ #(s - x - 1) }} )
+| read_ne_app :
+  `( {{ Rne m in s ↘ M }} ->
+     {{ Rnf n in s ↘ N }} ->
+     {{ Rne m n in s ↘ M N }} )
+| read_ne_natrec :
+  (* Nf of motive *)
+  `( {{ ⟦ B ⟧ p ↦ ⇑! ℕ s ↘ b }} ->
+     {{ Rtyp b in S s ↘ B' }} ->
+
+     (* Nf of mz *)
+     {{ ⟦ B ⟧ p ↦ zero ↘ bz }} ->
+     {{ Rnf ⇓ bz mz in s ↘ MZ }} ->
+
+     (* Nf of MS *)
+     {{ ⟦ B ⟧ p ↦ succ (⇑! ℕ s) ↘ bs }} ->
+     {{ ⟦ MS ⟧ p ↦ ⇑! ℕ s ↦ ⇑! b (S s) ↘ ms }} ->
+     {{ Rnf ⇓ bs ms in S (S s) ↘ MS' }} ->
+
+     (* Ne of m *)
+     {{ Rne m in s ↘ M }} ->
+
+     {{ Rne rec m under p return B | zero -> mz | succ -> MS end in s ↘ rec M return B' | zero -> MZ | succ -> MS' end }} )
+where "'Rne' m 'in' s ↘ M" := (read_ne s m M) (in custom judg) : type_scope
+with read_typ : nat -> domain -> nf -> Prop :=
+| read_typ_univ :
+  `( {{ Rtyp 𝕌@i in s ↘ Type@i }} )
+| read_typ_nat :
+  `( {{ Rtyp ℕ in s ↘ ℕ }} )
+| read_typ_pi :
+  (* Nf of arg type *)
+  `( {{ Rtyp a in s ↘ A }} ->
+
+     (* Nf of ret type *)
+     {{ ⟦ B ⟧ p ↦ ⇑! a s ↘ b }} ->
+     {{ Rtyp b in S s ↘ B' }} ->
+
+     {{ Rtyp Π a p B in s ↘ Π A B' }})
+| read_typ_neut :
+  `( {{ Rne b in s ↘ B }} ->
+     {{ Rtyp ⇑ a b in s ↘ ⇑ B }})
+where "'Rtyp' m 'in' s ↘ M" := (read_typ s m M) (in custom judg) : type_scope
+.
+
+Scheme read_nf_mut_ind := Induction for read_nf Sort Prop
+with read_ne_mut_ind := Induction for read_ne Sort Prop
+with read_typ_mut_ind := Induction for read_typ Sort Prop.
diff --git a/theories/Core/Semantic/ReadbackLemmas.v b/theories/Core/Semantic/ReadbackLemmas.v
index d1909e7e..30001af9 100644
--- a/theories/Core/Semantic/ReadbackLemmas.v
+++ b/theories/Core/Semantic/ReadbackLemmas.v
@@ -1,5 +1,6 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base Domain Evaluation EvaluationLemmas LibTactics Readback Syntax System.
+From Mcltt Require Import Base EvaluationLemmas LibTactics ReadbackDefinitions.
+Import Domain_Notations.
 
 Section functional_read.
   Let functional_read_nf_prop s m M1 (_ : {{ Rnf m in s ↘ M1 }}) : Prop := forall M2 (Hread2: {{ Rnf m in s ↘ M2 }}), M1 = M2.
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
index 5106d4e7..02f840e6 100644
--- a/theories/Core/Semantic/Realizability.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -1,6 +1,8 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
-From Mcltt Require Import Base Domain Evaluation EvaluationLemmas LibTactics PER PERLemmas Syntax System.
+From Mcltt Require Import Base Evaluation LibTactics.
+From Mcltt Require Export PER.
+Import Domain_Notations.
 
 Lemma per_nat_then_per_top : forall {n m},
     {{ Dom n ≈ m ∈ per_nat }} ->
diff --git a/theories/Core/Syntactic/CtxEquiv.v b/theories/Core/Syntactic/CtxEquiv.v
index b20dab58..b58996a6 100644
--- a/theories/Core/Syntactic/CtxEquiv.v
+++ b/theories/Core/Syntactic/CtxEquiv.v
@@ -1,4 +1,5 @@
-From Mcltt Require Import Base LibTactics Syntax System SystemLemmas.
+From Mcltt Require Import Base LibTactics System.
+Import Syntax_Notations.
 
 #[local]
 Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper H :=
diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v
index 6f2a4c85..fcb1f2b3 100644
--- a/theories/Core/Syntactic/Presup.v
+++ b/theories/Core/Syntactic/Presup.v
@@ -1,4 +1,5 @@
-From Mcltt Require Import Base CtxEquiv LibTactics Relations Syntax System SystemLemmas.
+From Mcltt Require Import Base CtxEquiv LibTactics Relations System.
+Import Syntax_Notations.
 
 #[local]
 Ltac gen_presup_ctx H :=
diff --git a/theories/Core/Syntactic/Relations.v b/theories/Core/Syntactic/Relations.v
index 6a723a55..23f9fda5 100644
--- a/theories/Core/Syntactic/Relations.v
+++ b/theories/Core/Syntactic/Relations.v
@@ -1,5 +1,6 @@
 From Coq Require Import Setoid.
-From Mcltt Require Import Base CtxEquiv LibTactics Syntax System SystemLemmas.
+From Mcltt Require Import Base CtxEquiv LibTactics System.
+Import Syntax_Notations.
 
 Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
 Proof with solve [mauto].
diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v
index 59e37cab..940eb81e 100644
--- a/theories/Core/Syntactic/Syntax.v
+++ b/theories/Core/Syntactic/Syntax.v
@@ -64,36 +64,6 @@ Definition exp_to_num e :=
   | None => None
   end.
 
-#[global] Bind Scope exp_scope with exp.
-#[global] Bind Scope exp_scope with sub.
-Open Scope exp_scope.
-
-#[global] Declare Custom Entry exp.
-
-Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : exp_scope.
-Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : exp_scope.
-Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
-Notation "x" := x (in custom exp at level 0, x global) : exp_scope.
-Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : exp_scope.
-Notation "'λ' A e" := (a_fn A e) (in custom exp at level 0, A custom exp at level 0, e custom exp at level 60) : exp_scope.
-Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : exp_scope.
-Notation "'ℕ'" := a_nat (in custom exp) : exp_scope.
-Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0) : exp_scope.
-Notation "'Π' A B" := (a_pi A B) (in custom exp at level 0, A custom exp at level 0, B custom exp at level 60) : exp_scope.
-Notation "'zero'" := a_zero (in custom exp at level 0) : exp_scope.
-Notation "'succ' e" := (a_succ e) (in custom exp at level 0, e custom exp at level 0) : exp_scope.
-Notation "'rec' e 'return' A | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec A ez es e) (in custom exp at level 0, A custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : exp_scope.
-Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : exp_scope.
-Notation "'Id'" := a_id (in custom exp at level 0) : exp_scope.
-Notation "'Wk'" := a_weaken (in custom exp at level 0) : exp_scope.
-
-Infix "∘" := a_compose (in custom exp at level 40) : exp_scope.
-Infix ",," := a_extend (in custom exp at level 50) : exp_scope.
-Notation "'q' σ" := ({{{ σ ∘ Wk ,, # 0 }}}) (in custom exp at level 30) : exp_scope.
-
-Notation "⋅" := nil (in custom exp at level 0) : exp_scope.
-Notation "x , y" := (cons y x) (in custom exp at level 50) : exp_scope.
-
 Inductive nf : Set :=
 | nf_typ : nat -> nf
 | nf_nat : nf
@@ -108,26 +78,6 @@ with ne : Set :=
 | ne_var : nat -> ne
 .
 
-#[global] Declare Custom Entry nf.
-
-#[global] Bind Scope exp_scope with nf.
-#[global] Bind Scope exp_scope with ne.
-
-Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{'  x  '}}}'") : exp_scope.
-Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : exp_scope.
-Notation "~ x" := x (in custom nf at level 0, x constr at level 0) : exp_scope.
-Notation "x" := x (in custom nf at level 0, x global) : exp_scope.
-Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 0, A custom nf at level 0, e custom nf at level 60) : exp_scope.
-Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : exp_scope.
-Notation "'ℕ'" := nf_nat (in custom nf) : exp_scope.
-Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0) : exp_scope.
-Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 0, A custom nf at level 0, B custom nf at level 60) : exp_scope.
-Notation "'zero'" := nf_zero (in custom nf at level 0) : exp_scope.
-Notation "'succ' M" := (nf_succ M) (in custom nf at level 0, M custom nf at level 0) : exp_scope.
-Notation "'rec' M 'return' A | 'zero' -> MZ | 'succ' -> MS 'end'" := (ne_natrec A MZ MS M) (in custom nf at level 0, A custom nf at level 60, MZ custom nf at level 60, MS custom nf at level 60, M custom nf at level 60) : exp_scope.
-Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0) : exp_scope.
-Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 0) : exp_scope.
-
 Fixpoint nf_to_exp (M : nf) : exp :=
   match M with
   | nf_typ i => a_typ i
@@ -148,3 +98,53 @@ with ne_to_exp (M : ne) : exp :=
 
 Coercion nf_to_exp : nf >-> exp.
 Coercion ne_to_exp : ne >-> exp.
+
+#[global] Declare Custom Entry exp.
+#[global] Declare Custom Entry nf.
+
+#[global] Bind Scope mcltt_scope with exp.
+#[global] Bind Scope mcltt_scope with sub.
+#[global] Bind Scope mcltt_scope with nf.
+#[global] Bind Scope mcltt_scope with ne.
+Open Scope mcltt_scope.
+
+Module Syntax_Notations.
+  Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : mcltt_scope.
+  Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : mcltt_scope.
+  Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : mcltt_scope.
+  Notation "x" := x (in custom exp at level 0, x global) : mcltt_scope.
+  Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : mcltt_scope.
+  Notation "'λ' A e" := (a_fn A e) (in custom exp at level 0, A custom exp at level 0, e custom exp at level 60) : mcltt_scope.
+  Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : mcltt_scope.
+  Notation "'ℕ'" := a_nat (in custom exp) : mcltt_scope.
+  Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'Π' A B" := (a_pi A B) (in custom exp at level 0, A custom exp at level 0, B custom exp at level 60) : mcltt_scope.
+  Notation "'zero'" := a_zero (in custom exp at level 0) : mcltt_scope.
+  Notation "'succ' e" := (a_succ e) (in custom exp at level 0, e custom exp at level 0) : mcltt_scope.
+  Notation "'rec' e 'return' A | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec A ez es e) (in custom exp at level 0, A custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : mcltt_scope.
+  Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'Id'" := a_id (in custom exp at level 0) : mcltt_scope.
+  Notation "'Wk'" := a_weaken (in custom exp at level 0) : mcltt_scope.
+
+  Infix "∘" := a_compose (in custom exp at level 40) : mcltt_scope.
+  Infix ",," := a_extend (in custom exp at level 50) : mcltt_scope.
+  Notation "'q' σ" := ({{{ σ ∘ Wk ,, # 0 }}}) (in custom exp at level 30) : mcltt_scope.
+
+  Notation "⋅" := nil (in custom exp at level 0) : mcltt_scope.
+  Notation "x , y" := (cons y x) (in custom exp at level 50) : mcltt_scope.
+
+  Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{'  x  '}}}'") : mcltt_scope.
+  Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : mcltt_scope.
+  Notation "~ x" := x (in custom nf at level 0, x constr at level 0) : mcltt_scope.
+  Notation "x" := x (in custom nf at level 0, x global) : mcltt_scope.
+  Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 0, A custom nf at level 0, e custom nf at level 60) : mcltt_scope.
+  Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : mcltt_scope.
+  Notation "'ℕ'" := nf_nat (in custom nf) : mcltt_scope.
+  Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 0, A custom nf at level 0, B custom nf at level 60) : mcltt_scope.
+  Notation "'zero'" := nf_zero (in custom nf at level 0) : mcltt_scope.
+  Notation "'succ' M" := (nf_succ M) (in custom nf at level 0, M custom nf at level 0) : mcltt_scope.
+  Notation "'rec' M 'return' A | 'zero' -> MZ | 'succ' -> MS 'end'" := (ne_natrec A MZ MS M) (in custom nf at level 0, A custom nf at level 60, MZ custom nf at level 60, MS custom nf at level 60, M custom nf at level 60) : mcltt_scope.
+  Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 0) : mcltt_scope.
+End Syntax_Notations.
diff --git a/theories/Core/Syntactic/System.v b/theories/Core/Syntactic/System.v
index 66182660..0e9ab2b1 100644
--- a/theories/Core/Syntactic/System.v
+++ b/theories/Core/Syntactic/System.v
@@ -1,294 +1 @@
-From Coq Require Import List.
-
-From Mcltt Require Import Base LibTactics Syntax.
-
-Reserved Notation "⊢ Γ" (in custom judg at level 80, Γ custom exp).
-Reserved Notation "⊢ Γ ≈ Γ'" (in custom judg at level 80, Γ custom exp, Γ' custom exp).
-Reserved Notation "Γ ⊢ M ≈ M' : A" (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
-Reserved Notation "Γ ⊢ M : A" (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
-Reserved Notation "Γ ⊢s σ : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).
-Reserved Notation "Γ ⊢s σ ≈ σ' : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
-Reserved Notation "'#' x : A ∈ Γ" (in custom judg at level 80, x constr at level 0, A custom exp, Γ custom exp at level 50).
-
-Generalizable All Variables.
-
-Inductive ctx_lookup : nat -> typ -> ctx -> Prop :=
-  | here : `({{ #0 : A[Wk] ∈ Γ , A }})
-  | there : `({{ #n : A ∈ Γ }} -> {{ #(S n) : A[Wk] ∈ Γ , B }})
-where "'#' x : A ∈ Γ" := (ctx_lookup x A Γ) (in custom judg) : type_scope.
-
-Inductive wf_ctx : ctx -> Prop :=
-| wf_ctx_empty : {{ ⊢ ⋅ }}
-| wf_ctx_extend :
-  `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ A : Type@i }} ->
-     {{ ⊢ Γ , A }} )
-where "⊢ Γ" := (wf_ctx Γ) (in custom judg) : type_scope
-with wf_ctx_eq : ctx -> ctx -> Prop :=
-| wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}
-| wf_ctx_eq_extend :
-  `( {{ ⊢ Γ ≈ Δ }} ->
-     {{ Γ ⊢ A : Type@i }} ->
-     {{ Δ ⊢ A' : Type@i }} ->
-     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-     {{ Δ ⊢ A ≈ A' : Type@i }} ->
-     {{ ⊢ Γ , A ≈ Δ , A' }} )
-where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope
-with wf_exp : ctx -> exp -> typ -> Prop :=
-| wf_univ :
-  `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ Type@i : Type@(S i) }} )
-| wf_nat :
-  `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ ℕ : Type@i }} )
-| wf_zero :
-  `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢ zero : ℕ }} )
-| wf_succ :
-  `( {{ Γ ⊢ M : ℕ }} ->
-     {{ Γ ⊢ succ M : ℕ }} )
-| wf_natrec :
-  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
-     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
-     {{ Γ ⊢ M : ℕ }} ->
-     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end : A[Id,,M] }} )
-| wf_pi :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ B : Type@i }} ->
-     {{ Γ ⊢ Π A B : Type@i }} )
-| wf_fn :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ M : B }} ->
-     {{ Γ ⊢ λ A M : Π A B }} )
-| wf_app :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ B : Type@i }} ->
-     {{ Γ ⊢ M : Π A B }} ->
-     {{ Γ ⊢ N : A }} ->
-     {{ Γ ⊢ M N : B[Id,,N] }} )
-| wf_vlookup :
-  `( {{ ⊢ Γ }} ->
-     {{ #x : A ∈ Γ }} ->
-     {{ Γ ⊢ #x : A }} )
-| wf_exp_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ M : A }} ->
-     {{ Γ ⊢ M[σ] : A[σ] }} )
-| wf_conv :
-  `( {{ Γ ⊢ M : A }} ->
-     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-     {{ Γ ⊢ M : A' }} )
-| wf_cumu :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ A : Type@(S i) }} )
-where "Γ ⊢ M : A" := (wf_exp Γ M A) (in custom judg) : type_scope
-with wf_sub : ctx -> sub -> ctx -> Prop :=
-| wf_sub_id :
-  `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢s Id : Γ }} )
-| wf_sub_weaken :
-  `( {{ ⊢ Γ , A }} ->
-     {{ Γ , A ⊢s Wk : Γ }} )
-| wf_sub_compose :
-  `( {{ Γ1 ⊢s σ2 : Γ2 }} ->
-     {{ Γ2 ⊢s σ1 : Γ3 }} ->
-     {{ Γ1 ⊢s σ1 ∘ σ2 : Γ3 }} )
-| wf_sub_extend :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ M : A[σ] }} ->
-     {{ Γ ⊢s (σ ,, M) : Δ , A }} )
-| wf_sub_conv :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ ⊢ Δ ≈ Δ' }} ->
-     {{ Γ ⊢s σ : Δ' }} )
-where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope
-with wf_exp_eq : ctx -> exp -> exp -> typ -> Prop :=
-| wf_exp_eq_typ_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} )
-| wf_exp_eq_nat_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@i }} )
-| wf_exp_eq_zero_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Γ ⊢ zero[σ] ≈ zero : ℕ }} )
-| wf_exp_eq_succ_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ M : ℕ }} ->
-     {{ Γ ⊢ (succ M)[σ] ≈ succ (M[σ]) : ℕ }} )
-| wf_exp_eq_succ_cong :
-  `( {{ Γ ⊢ M ≈ M' : ℕ }} ->
-     {{ Γ ⊢ succ M ≈ succ M' : ℕ }} )
-| wf_exp_eq_natrec_cong :
-  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
-     {{ Γ , ℕ ⊢ A ≈ A' : Type@i }} ->
-     {{ Γ ⊢ MZ ≈ MZ' : A[Id,,zero] }} ->
-     {{ Γ , ℕ , A ⊢ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
-     {{ Γ ⊢ M ≈ M' : ℕ }} ->
-     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end ≈ rec M' return A' | zero -> MZ' | succ -> MS' end : A[Id,,M] }} )
-| wf_exp_eq_natrec_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ , ℕ ⊢ A : Type@i }} ->
-     {{ Δ ⊢ MZ : A[Id,,zero] }} ->
-     {{ Δ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
-     {{ Δ ⊢ M : ℕ }} ->
-     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] ≈ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }} )
-| wf_exp_eq_nat_beta_zero :
-  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
-     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
-     {{ Γ ⊢ rec zero return A | zero -> MZ | succ -> MS end ≈ MZ : A[Id,,zero] }} )
-| wf_exp_eq_nat_beta_succ :
-  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
-     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
-     {{ Γ ⊢ M : ℕ }} ->
-     {{ Γ ⊢ rec (succ M) return A | zero -> MZ | succ -> MS end ≈ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }} )
-| wf_exp_eq_pi_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ A : Type@i }} ->
-     {{ Δ , A ⊢ B : Type@i }} ->
-     {{ Γ ⊢ (Π A B)[σ] ≈ Π (A[σ]) (B[q σ]) : Type@i }} )
-| wf_exp_eq_pi_cong :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-     {{ Γ , A ⊢ B ≈ B' : Type@i }} ->
-     {{ Γ ⊢ Π A B ≈ Π A' B' : Type@i }} )
-| wf_exp_eq_fn_cong :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-     {{ Γ , A ⊢ M ≈ M' : B }} ->
-     {{ Γ ⊢ λ A M ≈ λ A' M' : Π A B }} )
-| wf_exp_eq_fn_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ A : Type@i }} ->
-     {{ Δ , A ⊢ M : B }} ->
-     {{ Γ ⊢ (λ A M)[σ] ≈ λ A[σ] M[q σ] : (Π A B)[σ] }} )
-| wf_exp_eq_app_cong :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ B : Type@i }} ->
-     {{ Γ ⊢ M ≈ M' : Π A B }} ->
-     {{ Γ ⊢ N ≈ N' : A }} ->
-     {{ Γ ⊢ M N ≈ M' N' : B[Id,,N] }} )
-| wf_exp_eq_app_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ A : Type@i }} ->
-     {{ Δ , A ⊢ B : Type@i }} ->
-     {{ Δ ⊢ M : Π A B }} ->
-     {{ Δ ⊢ N : A }} ->
-     {{ Γ ⊢ (M N)[σ] ≈ M[σ] N[σ] : B[σ,,N[σ]] }} )
-| wf_exp_eq_pi_beta :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ B : Type@i }} ->
-     {{ Γ , A ⊢ M : B }} ->
-     {{ Γ ⊢ N : A }} ->
-     {{ Γ ⊢ (λ A M) N ≈ M[Id,,N] : B[Id,,N] }} )
-| wf_exp_eq_pi_eta :
-  `( {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ , A ⊢ B : Type@i }} ->
-     {{ Γ ⊢ M : Π A B }} ->
-     {{ Γ ⊢ M ≈ λ A (M[Wk] #0) : Π A B }} )
-| wf_exp_eq_var :
-  `( {{ ⊢ Γ }} ->
-     {{ #x : A ∈ Γ }} ->
-     {{ Γ ⊢ #x ≈ #x : A }} )
-| wf_exp_eq_var_0_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ M : A[σ] }} ->
-     {{ Γ ⊢ #0[σ ,, M] ≈ M : A[σ] }} )
-| wf_exp_eq_var_S_sub :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Δ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ M : A[σ] }} ->
-     {{ #x : B ∈ Δ }} ->
-     {{ Γ ⊢ #(S x)[σ ,, M] ≈ #x[σ] : B[σ] }} )
-| wf_exp_eq_var_weaken :
-  `( {{ ⊢ Γ , B }} ->
-     {{ #x : A ∈ Γ }} ->
-     {{ Γ , B ⊢ #x[Wk] ≈ #(S x) : A[Wk] }} )
-| wf_exp_eq_sub_cong :
-  `( {{ Δ ⊢ M ≈ M' : A }} ->
-     {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-     {{ Γ ⊢ M[σ] ≈ M'[σ'] : A[σ] }} )
-| wf_exp_eq_sub_id :
-  `( {{ Γ ⊢ M : A }} ->
-     {{ Γ ⊢ M[Id] ≈ M : A }} )
-| wf_exp_eq_sub_compose :
-  `( {{ Γ ⊢s τ : Γ' }} ->
-     {{ Γ' ⊢s σ : Γ'' }} ->
-     {{ Γ'' ⊢ M : A }} ->
-     {{ Γ ⊢ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }} )
-| wf_exp_eq_cumu :
-  `( {{ Γ ⊢ A ≈ A' : Type@i }} ->
-     {{ Γ ⊢ A ≈ A' : Type@(S i) }} )
-| wf_exp_eq_conv :
-  `( {{ Γ ⊢ M ≈ M' : A }} ->
-     {{ Γ ⊢ A ≈ A' : Type@i }} ->
-     {{ Γ ⊢ M ≈ M' : A' }} )
-| wf_exp_eq_sym :
-  `( {{ Γ ⊢ M ≈ M' : A }} ->
-     {{ Γ ⊢ M' ≈ M : A }} )
-| wf_exp_eq_trans :
-  `( {{ Γ ⊢ M ≈ M' : A }} ->
-     {{ Γ ⊢ M' ≈ M'' : A }} ->
-     {{ Γ ⊢ M ≈ M'' : A }} )
-where "Γ ⊢ M ≈ M' : A" := (wf_exp_eq Γ M M' A) (in custom judg) : type_scope
-with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
-| wf_sub_eq_id :
-  `( {{ ⊢ Γ }} ->
-     {{ Γ ⊢s Id ≈ Id : Γ }} )
-| wf_sub_eq_weaken :
-  `( {{ ⊢ Γ , A }} ->
-     {{ Γ , A ⊢s Wk ≈ Wk : Γ }} )
-| wf_sub_eq_compose_cong :
-  `( {{ Γ ⊢s τ ≈ τ' : Γ' }} ->
-     {{ Γ' ⊢s σ ≈ σ' : Γ'' }} ->
-     {{ Γ ⊢s σ ∘ τ ≈ σ' ∘ τ' : Γ'' }} )
-| wf_sub_eq_extend_cong :
-  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-     {{ Δ ⊢ A : Type@i }} ->
-     {{ Γ ⊢ M ≈ M' : A[σ] }} ->
-     {{ Γ ⊢s (σ ,, M) ≈ (σ' ,, M') : Δ , A }} )
-| wf_sub_eq_id_compose_right :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Γ ⊢s Id ∘ σ ≈ σ : Δ }} )
-| wf_sub_eq_id_compose_left :
-  `( {{ Γ ⊢s σ : Δ }} ->
-     {{ Γ ⊢s σ ∘ Id ≈ σ : Δ }} )
-| wf_sub_eq_compose_assoc :
-  `( {{ Γ' ⊢s σ : Γ }} ->
-     {{ Γ'' ⊢s σ' : Γ' }} ->
-     {{ Γ''' ⊢s σ'' : Γ'' }} ->
-     {{ Γ''' ⊢s (σ ∘ σ') ∘ σ'' ≈ σ ∘ (σ' ∘ σ'') : Γ }} )
-| wf_sub_eq_extend_compose :
-  `( {{ Γ' ⊢s σ : Γ'' }} ->
-     {{ Γ'' ⊢ A : Type@i }} ->
-     {{ Γ' ⊢ M : A[σ] }} ->
-     {{ Γ ⊢s τ : Γ' }} ->
-     {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , A }} )
-| wf_sub_eq_p_extend :
-  `( {{ Γ' ⊢s σ : Γ }} ->
-     {{ Γ ⊢ A : Type@i }} ->
-     {{ Γ' ⊢ M : A[σ] }} ->
-     {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }} )
-| wf_sub_eq_extend :
-  `( {{ Γ' ⊢s σ : Γ , A }} ->
-     {{ Γ' ⊢s σ ≈ ((Wk ∘ σ) ,, #0[σ]) : Γ , A }} )
-| wf_sub_eq_sym :
-  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-     {{ Γ ⊢s σ' ≈ σ : Δ }} )
-| wf_sub_eq_trans :
-  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-     {{ Γ ⊢s σ' ≈ σ'' : Δ }} ->
-     {{ Γ ⊢s σ ≈ σ'' : Δ }} )
-| wf_sub_eq_conv :
-  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
-     {{ ⊢ Δ ≈ Δ' }} ->
-     {{ Γ ⊢s σ ≈ σ' : Δ' }} )
-where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ S1 S2 Δ) (in custom judg) : type_scope.
-
-#[export]
-Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_exp_eq wf_sub_eq ctx_lookup: mcltt.
+From Mcltt Require Export SystemDefinitions SystemLemmas.
diff --git a/theories/Core/Syntactic/SystemDefinitions.v b/theories/Core/Syntactic/SystemDefinitions.v
new file mode 100644
index 00000000..7c658736
--- /dev/null
+++ b/theories/Core/Syntactic/SystemDefinitions.v
@@ -0,0 +1,295 @@
+From Coq Require Import List.
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export Syntax.
+Import Syntax_Notations.
+
+Reserved Notation "⊢ Γ" (in custom judg at level 80, Γ custom exp).
+Reserved Notation "⊢ Γ ≈ Γ'" (in custom judg at level 80, Γ custom exp, Γ' custom exp).
+Reserved Notation "Γ ⊢ M ≈ M' : A" (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
+Reserved Notation "Γ ⊢ M : A" (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
+Reserved Notation "Γ ⊢s σ : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).
+Reserved Notation "Γ ⊢s σ ≈ σ' : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
+Reserved Notation "'#' x : A ∈ Γ" (in custom judg at level 80, x constr at level 0, A custom exp, Γ custom exp at level 50).
+
+Generalizable All Variables.
+
+Inductive ctx_lookup : nat -> typ -> ctx -> Prop :=
+  | here : `({{ #0 : A[Wk] ∈ Γ , A }})
+  | there : `({{ #n : A ∈ Γ }} -> {{ #(S n) : A[Wk] ∈ Γ , B }})
+where "'#' x : A ∈ Γ" := (ctx_lookup x A Γ) (in custom judg) : type_scope.
+
+Inductive wf_ctx : ctx -> Prop :=
+| wf_ctx_empty : {{ ⊢ ⋅ }}
+| wf_ctx_extend :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ A : Type@i }} ->
+     {{ ⊢ Γ , A }} )
+where "⊢ Γ" := (wf_ctx Γ) (in custom judg) : type_scope
+with wf_ctx_eq : ctx -> ctx -> Prop :=
+| wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}
+| wf_ctx_eq_extend :
+  `( {{ ⊢ Γ ≈ Δ }} ->
+     {{ Γ ⊢ A : Type@i }} ->
+     {{ Δ ⊢ A' : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Δ ⊢ A ≈ A' : Type@i }} ->
+     {{ ⊢ Γ , A ≈ Δ , A' }} )
+where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope
+with wf_exp : ctx -> exp -> typ -> Prop :=
+| wf_univ :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ Type@i : Type@(S i) }} )
+| wf_nat :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ ℕ : Type@i }} )
+| wf_zero :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ zero : ℕ }} )
+| wf_succ :
+  `( {{ Γ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ succ M : ℕ }} )
+| wf_natrec :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end : A[Id,,M] }} )
+| wf_pi :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ Π A B : Type@i }} )
+| wf_fn :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ M : B }} ->
+     {{ Γ ⊢ λ A M : Π A B }} )
+| wf_app :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ M : Π A B }} ->
+     {{ Γ ⊢ N : A }} ->
+     {{ Γ ⊢ M N : B[Id,,N] }} )
+| wf_vlookup :
+  `( {{ ⊢ Γ }} ->
+     {{ #x : A ∈ Γ }} ->
+     {{ Γ ⊢ #x : A }} )
+| wf_exp_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ M : A }} ->
+     {{ Γ ⊢ M[σ] : A[σ] }} )
+| wf_conv :
+  `( {{ Γ ⊢ M : A }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ M : A' }} )
+| wf_cumu :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ A : Type@(S i) }} )
+where "Γ ⊢ M : A" := (wf_exp Γ M A) (in custom judg) : type_scope
+with wf_sub : ctx -> sub -> ctx -> Prop :=
+| wf_sub_id :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢s Id : Γ }} )
+| wf_sub_weaken :
+  `( {{ ⊢ Γ , A }} ->
+     {{ Γ , A ⊢s Wk : Γ }} )
+| wf_sub_compose :
+  `( {{ Γ1 ⊢s σ2 : Γ2 }} ->
+     {{ Γ2 ⊢s σ1 : Γ3 }} ->
+     {{ Γ1 ⊢s σ1 ∘ σ2 : Γ3 }} )
+| wf_sub_extend :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M : A[σ] }} ->
+     {{ Γ ⊢s (σ ,, M) : Δ , A }} )
+| wf_sub_conv :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ ⊢ Δ ≈ Δ' }} ->
+     {{ Γ ⊢s σ : Δ' }} )
+where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope
+with wf_exp_eq : ctx -> exp -> exp -> typ -> Prop :=
+| wf_exp_eq_typ_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} )
+| wf_exp_eq_nat_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@i }} )
+| wf_exp_eq_zero_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢ zero[σ] ≈ zero : ℕ }} )
+| wf_exp_eq_succ_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ (succ M)[σ] ≈ succ (M[σ]) : ℕ }} )
+| wf_exp_eq_succ_cong :
+  `( {{ Γ ⊢ M ≈ M' : ℕ }} ->
+     {{ Γ ⊢ succ M ≈ succ M' : ℕ }} )
+| wf_exp_eq_natrec_cong :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ , ℕ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ MZ ≈ MZ' : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS ≈ MS' : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ M ≈ M' : ℕ }} ->
+     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end ≈ rec M' return A' | zero -> MZ' | succ -> MS' end : A[Id,,M] }} )
+| wf_exp_eq_natrec_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ , ℕ ⊢ A : Type@i }} ->
+     {{ Δ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Δ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Δ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ rec M return A | zero -> MZ | succ -> MS end[σ] ≈ rec M[σ] return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M[σ]] }} )
+| wf_exp_eq_nat_beta_zero :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ rec zero return A | zero -> MZ | succ -> MS end ≈ MZ : A[Id,,zero] }} )
+| wf_exp_eq_nat_beta_succ :
+  `( {{ Γ , ℕ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ MZ : A[Id,,zero] }} ->
+     {{ Γ , ℕ , A ⊢ MS : A[Wk∘Wk,,succ(#1)] }} ->
+     {{ Γ ⊢ M : ℕ }} ->
+     {{ Γ ⊢ rec (succ M) return A | zero -> MZ | succ -> MS end ≈ MS[Id,,M,,rec M return A | zero -> MZ | succ -> MS end] : A[Id,,succ M] }} )
+| wf_exp_eq_pi_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Δ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ (Π A B)[σ] ≈ Π (A[σ]) (B[q σ]) : Type@i }} )
+| wf_exp_eq_pi_cong :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ , A ⊢ B ≈ B' : Type@i }} ->
+     {{ Γ ⊢ Π A B ≈ Π A' B' : Type@i }} )
+| wf_exp_eq_fn_cong :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ , A ⊢ M ≈ M' : B }} ->
+     {{ Γ ⊢ λ A M ≈ λ A' M' : Π A B }} )
+| wf_exp_eq_fn_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Δ , A ⊢ M : B }} ->
+     {{ Γ ⊢ (λ A M)[σ] ≈ λ A[σ] M[q σ] : (Π A B)[σ] }} )
+| wf_exp_eq_app_cong :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : Π A B }} ->
+     {{ Γ ⊢ N ≈ N' : A }} ->
+     {{ Γ ⊢ M N ≈ M' N' : B[Id,,N] }} )
+| wf_exp_eq_app_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Δ , A ⊢ B : Type@i }} ->
+     {{ Δ ⊢ M : Π A B }} ->
+     {{ Δ ⊢ N : A }} ->
+     {{ Γ ⊢ (M N)[σ] ≈ M[σ] N[σ] : B[σ,,N[σ]] }} )
+| wf_exp_eq_pi_beta :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ , A ⊢ M : B }} ->
+     {{ Γ ⊢ N : A }} ->
+     {{ Γ ⊢ (λ A M) N ≈ M[Id,,N] : B[Id,,N] }} )
+| wf_exp_eq_pi_eta :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ M : Π A B }} ->
+     {{ Γ ⊢ M ≈ λ A (M[Wk] #0) : Π A B }} )
+| wf_exp_eq_var :
+  `( {{ ⊢ Γ }} ->
+     {{ #x : A ∈ Γ }} ->
+     {{ Γ ⊢ #x ≈ #x : A }} )
+| wf_exp_eq_var_0_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M : A[σ] }} ->
+     {{ Γ ⊢ #0[σ ,, M] ≈ M : A[σ] }} )
+| wf_exp_eq_var_S_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M : A[σ] }} ->
+     {{ #x : B ∈ Δ }} ->
+     {{ Γ ⊢ #(S x)[σ ,, M] ≈ #x[σ] : B[σ] }} )
+| wf_exp_eq_var_weaken :
+  `( {{ ⊢ Γ , B }} ->
+     {{ #x : A ∈ Γ }} ->
+     {{ Γ , B ⊢ #x[Wk] ≈ #(S x) : A[Wk] }} )
+| wf_exp_eq_sub_cong :
+  `( {{ Δ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Γ ⊢ M[σ] ≈ M'[σ'] : A[σ] }} )
+| wf_exp_eq_sub_id :
+  `( {{ Γ ⊢ M : A }} ->
+     {{ Γ ⊢ M[Id] ≈ M : A }} )
+| wf_exp_eq_sub_compose :
+  `( {{ Γ ⊢s τ : Γ' }} ->
+     {{ Γ' ⊢s σ : Γ'' }} ->
+     {{ Γ'' ⊢ M : A }} ->
+     {{ Γ ⊢ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }} )
+| wf_exp_eq_cumu :
+  `( {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ A ≈ A' : Type@(S i) }} )
+| wf_exp_eq_conv :
+  `( {{ Γ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢ A ≈ A' : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : A' }} )
+| wf_exp_eq_sym :
+  `( {{ Γ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢ M' ≈ M : A }} )
+| wf_exp_eq_trans :
+  `( {{ Γ ⊢ M ≈ M' : A }} ->
+     {{ Γ ⊢ M' ≈ M'' : A }} ->
+     {{ Γ ⊢ M ≈ M'' : A }} )
+where "Γ ⊢ M ≈ M' : A" := (wf_exp_eq Γ M M' A) (in custom judg) : type_scope
+with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
+| wf_sub_eq_id :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢s Id ≈ Id : Γ }} )
+| wf_sub_eq_weaken :
+  `( {{ ⊢ Γ , A }} ->
+     {{ Γ , A ⊢s Wk ≈ Wk : Γ }} )
+| wf_sub_eq_compose_cong :
+  `( {{ Γ ⊢s τ ≈ τ' : Γ' }} ->
+     {{ Γ' ⊢s σ ≈ σ' : Γ'' }} ->
+     {{ Γ ⊢s σ ∘ τ ≈ σ' ∘ τ' : Γ'' }} )
+| wf_sub_eq_extend_cong :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : A[σ] }} ->
+     {{ Γ ⊢s (σ ,, M) ≈ (σ' ,, M') : Δ , A }} )
+| wf_sub_eq_id_compose_right :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢s Id ∘ σ ≈ σ : Δ }} )
+| wf_sub_eq_id_compose_left :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢s σ ∘ Id ≈ σ : Δ }} )
+| wf_sub_eq_compose_assoc :
+  `( {{ Γ' ⊢s σ : Γ }} ->
+     {{ Γ'' ⊢s σ' : Γ' }} ->
+     {{ Γ''' ⊢s σ'' : Γ'' }} ->
+     {{ Γ''' ⊢s (σ ∘ σ') ∘ σ'' ≈ σ ∘ (σ' ∘ σ'') : Γ }} )
+| wf_sub_eq_extend_compose :
+  `( {{ Γ' ⊢s σ : Γ'' }} ->
+     {{ Γ'' ⊢ A : Type@i }} ->
+     {{ Γ' ⊢ M : A[σ] }} ->
+     {{ Γ ⊢s τ : Γ' }} ->
+     {{ Γ ⊢s (σ ,, M) ∘ τ ≈ ((σ ∘ τ) ,, M[τ]) : Γ'' , A }} )
+| wf_sub_eq_p_extend :
+  `( {{ Γ' ⊢s σ : Γ }} ->
+     {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ' ⊢ M : A[σ] }} ->
+     {{ Γ' ⊢s Wk ∘ (σ ,, M) ≈ σ : Γ }} )
+| wf_sub_eq_extend :
+  `( {{ Γ' ⊢s σ : Γ , A }} ->
+     {{ Γ' ⊢s σ ≈ ((Wk ∘ σ) ,, #0[σ]) : Γ , A }} )
+| wf_sub_eq_sym :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Γ ⊢s σ' ≈ σ : Δ }} )
+| wf_sub_eq_trans :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Γ ⊢s σ' ≈ σ'' : Δ }} ->
+     {{ Γ ⊢s σ ≈ σ'' : Δ }} )
+| wf_sub_eq_conv :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ ⊢ Δ ≈ Δ' }} ->
+     {{ Γ ⊢s σ ≈ σ' : Δ' }} )
+where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ S1 S2 Δ) (in custom judg) : type_scope.
+
+#[export]
+Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_exp_eq wf_sub_eq ctx_lookup: mcltt.
diff --git a/theories/Core/Syntactic/SystemLemmas.v b/theories/Core/Syntactic/SystemLemmas.v
index 002fdc5a..ff657031 100644
--- a/theories/Core/Syntactic/SystemLemmas.v
+++ b/theories/Core/Syntactic/SystemLemmas.v
@@ -1,4 +1,5 @@
-From Mcltt Require Import Base LibTactics System Syntax.
+From Mcltt Require Import Base LibTactics SystemDefinitions.
+Import Syntax_Notations.
 
 Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} /\ exists i, {{ Γ ⊢ A : Type@i }}.
 Proof with solve [mauto].
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 92fc6677..c714ab5f 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -1,15 +1,18 @@
 -R . Mcltt
 
--arg -w -arg -notation-overridden
+-arg -w -arg -cast-in-pattern,-notation-overridden
 
 ./Core/Axioms.v
 ./Core/Base.v
 ./Core/Semantic/Domain.v
 ./Core/Semantic/Evaluation.v
+./Core/Semantic/EvaluationDefinitions.v
 ./Core/Semantic/EvaluationLemmas.v
 ./Core/Semantic/PER.v
+./Core/Semantic/PERDefinitions.v
 ./Core/Semantic/PERLemmas.v
 ./Core/Semantic/Readback.v
+./Core/Semantic/ReadbackDefinitions.v
 ./Core/Semantic/ReadbackLemmas.v
 ./Core/Semantic/Realizability.v
 ./Core/Syntactic/CtxEquiv.v
@@ -17,6 +20,7 @@
 ./Core/Syntactic/Relations.v
 ./Core/Syntactic/Syntax.v
 ./Core/Syntactic/System.v
+./Core/Syntactic/SystemDefinitions.v
 ./Core/Syntactic/SystemLemmas.v
 ./Frontend/Elaborator.v
 ./Frontend/Parser.v