diff --git a/theories/Core/Axioms.v b/theories/Core/Axioms.v
new file mode 100644
index 00000000..1602d351
--- /dev/null
+++ b/theories/Core/Axioms.v
@@ -0,0 +1,42 @@
+Require Export Coq.Logic.PropExtensionality.
+Require Export Coq.Logic.IndefiniteDescription.
+Require Export Coq.Logic.FunctionalExtensionality.
+
+
+Lemma dep_functional_choice :
+  forall (A : Type) (B : A -> Type) (R: forall a, B a -> Prop),
+    (forall x : A, exists y : B x, R x y) ->
+    (exists f : forall x, B x, forall x : A, R x (f x)).
+Proof.
+  intros.
+  exists (fun x => proj1_sig (constructive_indefinite_description (R x) (H x))).
+  intro x.
+  apply (proj2_sig (constructive_indefinite_description (R x) (H x))).
+Qed.
+
+Lemma dep_functional_choice_equiv :
+  forall (A : Type) (B : A -> Type) (R: forall a, B a -> Prop),
+    (forall x : A, exists y : B x, R x y) <->
+    (exists f : forall x, B x, forall x : A, R x (f x)).
+Proof.
+  intros; split.
+  - apply dep_functional_choice.
+  - firstorder.
+Qed.
+
+Lemma functional_choice_equiv :
+  forall (A B : Type) (R:A->B->Prop),
+    (forall x : A, exists y : B, R x y) <->
+    (exists f : A->B, forall x : A, R x (f x)).
+Proof.
+  intros; split.
+  - apply functional_choice.
+  - firstorder.
+Qed.
+
+Lemma exists_absorption :
+  forall (A : Type) (P : A -> Prop) (Q : Prop),
+    (exists x : A, P x) /\ Q <-> (exists x : A, P x /\ Q).
+Proof.
+  firstorder.
+Qed.
diff --git a/theories/Core/Semantic/EvaluateLemmas.v b/theories/Core/Semantic/EvaluateLemmas.v
new file mode 100644
index 00000000..81262155
--- /dev/null
+++ b/theories/Core/Semantic/EvaluateLemmas.v
@@ -0,0 +1,67 @@
+From Coq Require Import Lia PeanoNat Relations.
+From Mcltt Require Import Base Domain Evaluate LibTactics Syntax System.
+
+Section functional_eval.
+  Let functional_eval_exp_prop M p m1 (_ : {{ ⟦ M ⟧ p ↘ m1 }}) : Prop := forall m2 (Heval2: {{ ⟦ M ⟧ p ↘ m2 }}), m1 = m2.
+  Let functional_eval_natrec_prop A MZ MS m p r1 (_ : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }}) : Prop := forall r2 (Heval2 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r2 }}), r1 = r2.
+  Let functional_eval_app_prop m n r1 (_ : {{ $| m & n |↘ r1 }}) : Prop := forall r2 (Heval2 : {{ $| m & n |↘ r2 }}), r1 = r2.
+  Let functional_eval_sub_prop σ p p1 (_ : {{ ⟦ σ ⟧s p ↘ p1 }}) : Prop := forall p2 (Heval2 : {{ ⟦ σ ⟧s p ↘ p2 }}), p1 = p2.
+
+  #[local]
+  Ltac unfold_functional_eval := unfold functional_eval_exp_prop, functional_eval_natrec_prop, functional_eval_app_prop, functional_eval_sub_prop in *.
+
+  Lemma functional_eval_exp : forall M p m1 (Heval1 : {{ ⟦ M ⟧ p ↘ m1 }}), functional_eval_exp_prop M p m1 Heval1.
+  Proof using.
+    intros *.
+    induction Heval1
+      using eval_exp_mut_ind
+      with (P0 := functional_eval_natrec_prop)
+           (P1 := functional_eval_app_prop)
+           (P2 := functional_eval_sub_prop);
+      unfold_functional_eval; mauto;
+      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
+      solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1_1, IHHeval1_2 in *; mauto].
+  Qed.
+
+  Lemma functional_eval_natrec : forall A MZ MS m p r1 (Heval1 : {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r1 }}), functional_eval_natrec_prop A MZ MS m p r1 Heval1.
+  Proof using.
+    intros *.
+    induction Heval1
+      using eval_natrec_mut_ind
+      with (P := functional_eval_exp_prop)
+           (P1 := functional_eval_app_prop)
+           (P2 := functional_eval_sub_prop);
+      unfold_functional_eval; mauto;
+      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
+      solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1, IHHeval0 in *; mauto].
+  Qed.
+
+  Lemma functional_eval_app : forall m n r1 (Heval1 : {{ $| m & n |↘ r1 }}), functional_eval_app_prop m n r1 Heval1.
+  Proof using.
+    intros *.
+    induction Heval1
+      using eval_app_mut_ind
+      with (P := functional_eval_exp_prop)
+           (P0 := functional_eval_natrec_prop)
+           (P2 := functional_eval_sub_prop);
+      unfold_functional_eval; mauto;
+      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
+      solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1, IHHeval0 in *; mauto].
+  Qed.
+
+  Lemma functional_eval_sub : forall σ p p1 (Heval1 : {{ ⟦ σ ⟧s p ↘ p1 }}), functional_eval_sub_prop σ p p1 Heval1.
+  Proof using.
+    intros *.
+    induction Heval1
+      using eval_sub_mut_ind
+      with (P := functional_eval_exp_prop)
+           (P0 := functional_eval_natrec_prop)
+           (P1 := functional_eval_app_prop);
+      unfold_functional_eval; mauto;
+      intros; inversion Heval2; clear Heval2; subst; do 2 f_equal;
+      try solve [mauto|erewrite IHHeval1 in *; mauto|erewrite IHHeval1, IHHeval0 in *; mauto|erewrite IHHeval1_1 in *; mauto].
+  Qed.
+End functional_eval.
+
+#[export]
+Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_sub : mcltt.
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
new file mode 100644
index 00000000..be6a3a1c
--- /dev/null
+++ b/theories/Core/Semantic/PER.v
@@ -0,0 +1,223 @@
+From Coq Require Import Lia PeanoNat Relations.
+From Equations Require Import Equations.
+From Mcltt Require Import Base Domain Evaluate Readback Syntax System.
+
+Notation "'Dom' a ≈ b ∈ R" := (R a b : 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) (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) (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) (in custom judg at level 90, a custom exp, b custom exp, R constr, R' constr).
+
+Generalizable All Variables.
+
+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'.
+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'.
+Arguments mk_rel_mod_app {_ _ _ _ _}.
+
+Definition per_bot : relation domain_ne := fun m n => (forall s, exists L, {{ Rne m in s ↘ L }} /\ {{ Rne n in s ↘ L }}).
+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 }}).
+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 }}).
+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 }} }
+.
+
+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}}),
+          (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 :
+    `{ {{ 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 ->
+        (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'}, 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 }} :=
+    per_univ_elem_core_strong_ind a b R (per_univ_elem_core_univ lt_j_i eq) := case_U _ _ lt_j_i eq;
+    per_univ_elem_core_strong_ind a b R per_univ_elem_core_nat := case_nat;
+    per_univ_elem_core_strong_ind a b R
+      (per_univ_elem_core_pi in_rel out_rel equiv_a_a' HT HE) :=
+          case_Pi out_rel equiv_a_a' (per_univ_elem_core_strong_ind _ _ _ equiv_a_a')
+            (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;
+    per_univ_elem_core_strong_ind a b R per_univ_elem_core_neut :=  case_ne.
+
+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' }}.
+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.
+
+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 ->
+        (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'}, 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 :=
+    per_univ_elem_ind' 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 HT HE => case_Pi i out_rel _ IHA _ 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 :=
+    per_univ_elem_ind i a b R H := per_univ_elem_ind' i a b R _.
+
+End Per_univ_elem_ind_def.
+
+Lemma rel_mod_eval_ex_pull :
+  forall (A : Type) (P : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R,
+    rel_mod_eval (fun a b R => exists x : A, P a b R x) T p T' p' R <->
+      exists x : A, rel_mod_eval (fun a b R => P a b R x) T p T' p' R.
+Proof.
+  split; intros.
+  - destruct H.
+    destruct H1 as [? ?].
+    eexists; econstructor; eauto.
+  - do 2 destruct H; econstructor; eauto.
+Qed.
+
+Lemma rel_mod_eval_simp_ex :
+  forall (A : Type) (P : domain -> domain -> relation domain -> Prop) (Q : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R,
+    rel_mod_eval (fun a b R => P a b R /\ exists x : A, Q a b R x) T p T' p' R <->
+      exists x : A, rel_mod_eval (fun a b R => P a b R /\ Q a b R x) T p T' p' R.
+Proof.
+  split; intros.
+  - destruct H.
+    destruct H1 as [? [? ?]].
+    eexists; econstructor; eauto.
+  - do 2 destruct H; econstructor; eauto.
+    firstorder.
+Qed.
+
+Lemma rel_mod_eval_simp_and :
+  forall (P : domain -> domain -> relation domain -> Prop) (Q : relation domain -> Prop) {T p T' p'} R,
+    rel_mod_eval (fun a b R => P a b R /\ Q R) T p T' p' R <->
+      rel_mod_eval P T p T' p' R /\ Q R.
+Proof.
+  split; intros.
+  - destruct H.
+    destruct H1 as [? ?].
+    split; try econstructor; eauto.
+  - do 2 destruct H; econstructor; eauto.
+Qed.
+
+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
new file mode 100644
index 00000000..5bcbde2a
--- /dev/null
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -0,0 +1,188 @@
+From Coq Require Import Lia PeanoNat Relations ChoiceFacts Program.Equality.
+From Equations Require Import Equations.
+From Mcltt Require Import Axioms Base Domain Evaluate EvaluateLemmas LibTactics PER Readback ReadbackLemmas Syntax System.
+
+Lemma per_bot_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_bot }} ->
+    {{ Dom n ≈ m ∈ per_bot }}.
+Proof with mauto.
+  intros * H s.
+  destruct (H s) as [? []]...
+Qed.
+
+#[export]
+Hint Resolve per_bot_sym : mcltt.
+
+Lemma per_bot_trans : forall m n l,
+    {{ Dom m ≈ n ∈ per_bot }} ->
+    {{ Dom n ≈ l ∈ per_bot }} ->
+    {{ Dom m ≈ l ∈ per_bot }}.
+Proof.
+  intros * Hmn Hnl s.
+  destruct (Hmn s) as [L []].
+  destruct (Hnl s) as [L' []].
+  replace L' with L in *; mauto.
+Qed.
+
+#[export]
+Hint Resolve per_bot_trans : mcltt.
+
+Lemma per_nat_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_nat }} ->
+    {{ Dom n ≈ m ∈ per_nat }}.
+Proof.
+  intros *.
+  induction 1; econstructor; mauto.
+Qed.
+
+#[export]
+Hint Resolve per_nat_sym : mcltt.
+
+Lemma per_nat_trans : forall m n l,
+    {{ Dom m ≈ n ∈ per_nat }} ->
+    {{ Dom n ≈ l ∈ per_nat }} ->
+    {{ Dom m ≈ l ∈ per_nat }}.
+Proof.
+  intros * H. gen l.
+  induction H; intros * H'; inversion_clear H'; econstructor; mauto.
+Qed.
+
+#[export]
+Hint Resolve per_nat_trans : mcltt.
+
+Lemma per_ne_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_ne }} ->
+    {{ Dom n ≈ m ∈ per_ne }}.
+Proof.
+  intros * [].
+  econstructor.
+  mauto.
+Qed.
+
+#[export]
+Hint Resolve per_ne_sym : mcltt.
+
+Lemma per_ne_trans : forall m n l,
+    {{ Dom m ≈ n ∈ per_ne }} ->
+    {{ Dom n ≈ l ∈ per_ne }} ->
+    {{ Dom m ≈ l ∈ per_ne }}.
+Proof with mauto.
+  intros * [] Hnl.
+  inversion_clear Hnl.
+  econstructor...
+Qed.
+
+#[export]
+Hint Resolve per_ne_trans : mcltt.
+
+Lemma per_univ_elem_right_irrel_gen : forall i A B R,
+    per_univ_elem i A B R ->
+    forall A' B' R',
+      A = A' ->
+      per_univ_elem i A' B' R' ->
+      R = R'.
+Proof.
+  induction 1 using per_univ_elem_ind; intros * Heq Hright;
+    try solve [induction Hright using per_univ_elem_ind; congruence].
+  subst.
+  simp per_univ_elem in Hright; inversion Hright; try congruence; subst.
+  rewrite <- per_univ_elem_equation_1 in *.
+  specialize (IHper_univ_elem _ _ _ eq_refl equiv_a_a').
+  subst.
+  extensionality f.
+  extensionality f'.
+  rewrite H1, H8.
+  extensionality c.
+  extensionality c'.
+  extensionality equiv_c_c'.
+  specialize (H0 _ _ equiv_c_c') as [a ? ? ? [? ?]].
+  specialize (H7 _ _ equiv_c_c') as [a0 ? ? ? ?].
+  replace a0 with a in * by mauto.
+  specialize (H4 _ _ _ eq_refl H7).
+  congruence.
+Qed.
+
+Lemma per_univ_elem_right_irrel : forall i A B R B' R',
+    per_univ_elem i A B R ->
+    per_univ_elem i A B' R' ->
+    R = R'.
+Proof.
+  intros. eauto using per_univ_elem_right_irrel_gen.
+Qed.
+
+Lemma per_univ_elem_sym : forall i A B R,
+    per_univ_elem i A B R ->
+    exists R', per_univ_elem i B A R' /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R' }}).
+Proof.
+  intros. induction H using per_univ_elem_ind; subst.
+  - exists (per_univ j'). split.
+    + apply per_univ_elem_core_univ'; trivial.
+    + intros. split; intros HD; destruct HD.
+      * specialize (H1 _ _ _ H0).
+        firstorder.
+      * specialize (H1 _ _ _ H0).
+        firstorder.
+  - exists per_nat. split.
+    + econstructor.
+    + intros; split; mauto.
+  - destruct IHper_univ_elem as [in_rel' [? ?]].
+    setoid_rewrite rel_mod_eval_simp_ex in H0.
+    repeat setoid_rewrite dep_functional_choice_equiv in H0.
+    destruct H0 as [out_rel' ?].
+    assert (forall a b : domain, in_rel' a b -> in_rel b a) as Hconv by firstorder.
+    assert (forall a b : domain, in_rel a b -> in_rel' b a) as Hconv' by firstorder.
+    setoid_rewrite H1.
+    exists (fun f f' => forall (c c' : domain) (equiv_c_c' : in_rel' c c'), rel_mod_app (out_rel' c' c (Hconv _ _ equiv_c_c')) f c f' c').
+    split.
+    + simp per_univ_elem; econstructor; try rewrite <- per_univ_elem_equation_1 in *; eauto.
+      * intros.
+        destruct (H0 _ _ (Hconv _ _ equiv_c_c')) as [? ? ? ? [? [? ?]]].
+        econstructor; eauto.
+        apply H7.
+      * auto.
+    + split; intros.
+      * destruct (H0 _ _ (Hconv _ _ equiv_c_c')) as [? ? ? ? [? [? ?]]].
+        specialize (H4 _ _ (Hconv c c' equiv_c_c')) as [].
+        econstructor; eauto; firstorder.
+      * destruct (H0 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
+        specialize (H4 _ _ (Hconv' _ _ equiv_c_c')) as [].
+        econstructor; eauto; firstorder.
+        replace (Hconv c' c (Hconv' c c' equiv_c_c')) with equiv_c_c' in H11 by apply proof_irrelevance.
+        firstorder.
+  - exists per_ne. split.
+    + econstructor.
+    + intros; split; mauto.
+Qed.
+
+(* 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 *. *)
+
+(* Lemma per_univ_elem_trans : forall i A1 A2 R1, *)
+(*     per_univ_elem i A1 A2 R1 -> *)
+(*     forall A3 R2, *)
+(*     per_univ_elem i A2 A3 R2 -> *)
+(*     exists R3, per_univ_elem i A1 A3 R3 /\ (forall a1 a2 a3, R1 a1 a2 -> R2 a2 a3 -> R3 a1 a3). *)
+(* Proof. *)
+(*   induction 1 using per_univ_elem_ind; intros ? ? HT2; *)
+(*     invert_per_univ_elem HT2. *)
+(*   - exists (per_univ j'0). *)
+(*     split. *)
+(*     + apply per_univ_elem_core_univ'; trivial. *)
+(*     + intros. unfold per_univ in *. *)
+(*       destruct H0, H2. *)
+(*       destruct (H1 _ _ _ H0 _ _ H2) as [? [? ?]]. *)
+(*       eauto. *)
+(*   - exists per_nat. *)
+(*     split... *)
+(*     + mauto. *)
+(*     + eapply per_nat_trans. *)
+(*   - specialize (IHper_univ_elem _ _ equiv_a_a'). *)
+(*     destruct IHper_univ_elem as [in_rel3 [? ?]]. *)
diff --git a/theories/Core/Semantic/Readback.v b/theories/Core/Semantic/Readback.v
index 13ad389b..d9f809ee 100644
--- a/theories/Core/Semantic/Readback.v
+++ b/theories/Core/Semantic/Readback.v
@@ -81,3 +81,7 @@ with read_typ : nat -> domain -> nf -> Prop :=
      {{ 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.
diff --git a/theories/Core/Semantic/ReadbackLemmas.v b/theories/Core/Semantic/ReadbackLemmas.v
new file mode 100644
index 00000000..18b50bc5
--- /dev/null
+++ b/theories/Core/Semantic/ReadbackLemmas.v
@@ -0,0 +1,65 @@
+From Coq Require Import Lia PeanoNat Relations.
+From Mcltt Require Import Base Domain Evaluate EvaluateLemmas LibTactics Readback Syntax System.
+
+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.
+  Let functional_read_ne_prop s m M1 (_ : {{ Rne m in s ↘ M1 }}) : Prop := forall M2 (Hread2 : {{ Rne m in s ↘ M2 }}), M1 = M2.
+  Let functional_read_typ_prop s m M1 (_ : {{ Rtyp m in s ↘ M1 }}) : Prop := forall M2 (Hread2 : {{ Rtyp m in s ↘ M2 }}), M1 = M2.
+
+  #[local]
+  Ltac unfold_functional_read := unfold functional_read_nf_prop, functional_read_ne_prop, functional_read_typ_prop in *.
+
+  Lemma functional_read_nf : forall s m M1 (Hread1: {{ Rnf m in s ↘ M1 }}), functional_read_nf_prop s m M1 Hread1.
+  Proof using Type with mauto .
+    intros *.
+    induction Hread1
+      using read_nf_mut_ind
+      with (P0 := functional_read_ne_prop)
+           (P1 := functional_read_typ_prop);
+      unfold_functional_read; mauto;
+      intros; inversion Hread2; clear Hread2; subst;
+      try replace m'0 with m' in * by mauto;
+      try replace b0 with b in * by mauto;
+      try replace bz0 with bz in * by mauto;
+      try replace bs0 with bs in * by mauto;
+      try replace ms0 with ms in * by mauto;
+      f_equal...
+  Qed.
+
+  Lemma functional_read_ne : forall s m M1 (Hread1 : {{ Rne m in s ↘ M1 }}), functional_read_ne_prop s m M1 Hread1.
+  Proof using Type with mauto.
+    intros *.
+    induction Hread1
+      using read_ne_mut_ind
+      with (P := functional_read_nf_prop)
+           (P1 := functional_read_typ_prop);
+      unfold_functional_read; mauto;
+      intros; inversion Hread2; clear Hread2; subst;
+      try replace m'0 with m' in * by mauto;
+      try replace b0 with b in * by mauto;
+      try replace bz0 with bz in * by mauto;
+      try replace bs0 with bs in * by mauto;
+      try replace ms0 with ms in * by mauto;
+      f_equal...
+  Qed.
+
+  Lemma functional_read_typ : forall s m M1 (Hread1 : {{ Rtyp m in s ↘ M1 }}), functional_read_typ_prop s m M1 Hread1.
+  Proof using Type with mauto.
+    intros *.
+    induction Hread1
+      using read_typ_mut_ind
+      with (P := functional_read_nf_prop)
+           (P0 := functional_read_ne_prop);
+      unfold_functional_read; mauto;
+      intros; inversion Hread2; clear Hread2; subst;
+      try replace m'0 with m' in * by mauto;
+      try replace b0 with b in * by mauto;
+      try replace bz0 with bz in * by mauto;
+      try replace bs0 with bs in * by mauto;
+      try replace ms0 with ms in * by mauto;
+      f_equal...
+  Qed.
+End functional_read.
+
+#[global]
+Hint Resolve functional_read_nf functional_read_ne functional_read_typ : mcltt.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index 82f5e936..98ccc535 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -2,10 +2,15 @@
 
 -arg -w -arg -notation-overridden
 
+./Core/Axioms.v
 ./Core/Base.v
 ./Core/Semantic/Domain.v
 ./Core/Semantic/Evaluate.v
+./Core/Semantic/EvaluateLemmas.v
+./Core/Semantic/PER.v
+./Core/Semantic/PERLemmas.v
 ./Core/Semantic/Readback.v
+./Core/Semantic/ReadbackLemmas.v
 ./Core/Syntactic/CtxEquiv.v
 ./Core/Syntactic/Presup.v
 ./Core/Syntactic/Relations.v