diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index e749f9a8..b49b2b3f 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -1 +1 @@
-From Mcltt Require Export PERDefinitions PERLemmas.
+From Mcltt Require Export PERBasicLemmas PERDefinitions PERLemmas.
diff --git a/theories/Core/Semantic/PERBasicLemmas.v b/theories/Core/Semantic/PERBasicLemmas.v
new file mode 100644
index 00000000..30399aca
--- /dev/null
+++ b/theories/Core/Semantic/PERBasicLemmas.v
@@ -0,0 +1,354 @@
+From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
+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, *)
+(*     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. *)
+
+Lemma per_bot_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_bot }} ->
+    {{ Dom n ≈ m ∈ per_bot }}.
+Proof with solve [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 with solve [mauto].
+  intros * Hmn Hnl s.
+  destruct (Hmn s) as [? []].
+  destruct (Hnl s) as [? []].
+  functional_read_rewrite_clear...
+Qed.
+
+#[export]
+Hint Resolve per_bot_trans : mcltt.
+
+Lemma var_per_bot : forall {n},
+    {{ Dom !n ≈ !n ∈ per_bot }}.
+Proof.
+  intros n s. repeat econstructor.
+Qed.
+
+#[export]
+Hint Resolve var_per_bot : mcltt.
+
+Lemma per_top_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_top }} ->
+    {{ Dom n ≈ m ∈ per_top }}.
+Proof with solve [mauto].
+  intros * H s.
+  destruct (H s) as [? []]...
+Qed.
+
+#[export]
+Hint Resolve per_top_sym : mcltt.
+
+Lemma per_top_trans : forall m n l,
+    {{ Dom m ≈ n ∈ per_top }} ->
+    {{ Dom n ≈ l ∈ per_top }} ->
+    {{ Dom m ≈ l ∈ per_top }}.
+Proof with solve [mauto].
+  intros * Hmn Hnl s.
+  destruct (Hmn s) as [? []].
+  destruct (Hnl s) as [? []].
+  functional_read_rewrite_clear...
+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 }}.
+Proof with solve [mauto].
+  intros * H s.
+  destruct (H s) as [? []]...
+Qed.
+
+#[export]
+Hint Resolve per_top_typ_sym : mcltt.
+
+Lemma per_top_typ_trans : forall m n l,
+    {{ Dom m ≈ n ∈ per_top_typ }} ->
+    {{ Dom n ≈ l ∈ per_top_typ }} ->
+    {{ Dom m ≈ l ∈ per_top_typ }}.
+Proof with solve [mauto].
+  intros * Hmn Hnl s.
+  destruct (Hmn s) as [? []].
+  destruct (Hnl s) as [? []].
+  functional_read_rewrite_clear...
+Qed.
+
+#[export]
+Hint Resolve per_top_typ_trans : mcltt.
+
+Lemma PER_per_top_typ : PER per_top_typ.
+Proof with solve [mauto].
+  econstructor...
+Qed.
+
+Lemma per_nat_sym : forall m n,
+    {{ Dom m ≈ n ∈ per_nat }} ->
+    {{ Dom n ≈ m ∈ per_nat }}.
+Proof with solve [mauto].
+  induction 1; econstructor...
+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 with solve [mauto].
+  intros * H. gen l.
+  induction H; intros * H'; inversion_clear H'; econstructor...
+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 with solve [mauto].
+  intros * [].
+  econstructor...
+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 solve [mauto].
+  intros * [] Hnl.
+  inversion_clear Hnl.
+  econstructor...
+Qed.
+
+#[export]
+Hint Resolve per_ne_trans : mcltt.
+
+Lemma per_univ_elem_right_irrel : forall i i' A B R B' R',
+    per_univ_elem i A B R ->
+    per_univ_elem i' A B' R' ->
+    R = R'.
+Proof.
+  intros * Horig.
+  remember A as A' in |- *.
+  gen A' B' R'.
+  induction Horig using per_univ_elem_ind; intros * Heq Hright;
+    try solve [induction Hright using per_univ_elem_ind; congruence].
+  subst.
+  invert_per_univ_elem Hright; try congruence.
+  specialize (IHHorig _ _ _ eq_refl equiv_a_a').
+  subst.
+  extensionality f.
+  extensionality f'.
+  rewrite H2, H10.
+  extensionality c.
+  extensionality c'.
+  extensionality equiv_c_c'.
+  destruct_rel_mod_eval.
+  functional_eval_rewrite_clear.
+  specialize (H12 _ _ _ eq_refl H5).
+  congruence.
+Qed.
+
+Ltac per_univ_elem_right_irrel_rewrite1 :=
+  match goal with
+  | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+      clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
+  end.
+Ltac per_univ_elem_right_irrel_rewrite := repeat per_univ_elem_right_irrel_rewrite1.  
+
+Lemma per_univ_elem_sym : forall i A B R,
+    per_univ_elem i A B R ->
+    per_univ_elem i B A R /\ (forall a b, {{ Dom a ≈ b ∈ R }} -> {{ Dom b ≈ a ∈ R }}).
+Proof.
+  induction 1 using per_univ_elem_ind; subst.
+  - split.
+    + apply per_univ_elem_core_univ'; trivial.
+    + intros * [].
+      specialize (H1 _ _ _ H0).
+      firstorder.
+  - split.
+    + econstructor.
+    + intros; mauto.
+  - destruct IHper_univ_elem as [? ?].
+    setoid_rewrite H2.
+    split.
+    + per_univ_elem_econstructor; eauto.
+      intros.
+      assert (equiv_c'_c : in_rel c' c) by firstorder.
+      assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
+      destruct_rel_mod_eval.
+      econstructor; eauto.
+      functional_eval_rewrite_clear.
+      per_univ_elem_right_irrel_rewrite.
+      assumption.
+    + assert (forall a b : domain,
+                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') a c b c') ->
+                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')).
+      {
+        intros.
+        assert (equiv_c'_c : in_rel c' c) by firstorder.
+        assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
+        destruct_rel_mod_eval.
+        destruct_rel_mod_app.
+        functional_eval_rewrite_clear.
+        per_univ_elem_right_irrel_rewrite.
+        econstructor; eauto.
+      }
+      firstorder.
+  - split.
+    + econstructor; mauto.
+    + intros; mauto.
+Qed.
+
+Lemma per_univ_elem_left_irrel : forall i i' A B R A' R',
+    per_univ_elem i A B R ->
+    per_univ_elem i' A' B R' ->
+    R = R'.
+Proof.
+  intros * []%per_univ_elem_sym []%per_univ_elem_sym.
+  eauto using per_univ_elem_right_irrel.
+Qed.
+
+Lemma per_univ_elem_cross_irrel : forall i i' A B R B' R',
+    per_univ_elem i A B R ->
+    per_univ_elem i' B' A R' ->
+    R = R'.
+Proof.
+  intros * ? []%per_univ_elem_sym.
+  eauto using per_univ_elem_right_irrel.
+Qed.
+
+Ltac do_per_univ_elem_irrel_rewrite1 :=
+  match goal with
+    | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
+        H2 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+        clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
+    | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
+        H2 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+        clean replace R2 with R1 by (eauto using per_univ_elem_left_irrel)
+    | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
+        H2 : {{ DF ~_ ≈ ~?A ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+        (* Order matters less here as H1 and H2 cannot be exchanged *)
+        clean replace R2 with R1 by (symmetry; eauto using per_univ_elem_cross_irrel)
+    end.
+
+Ltac do_per_univ_elem_irrel_rewrite :=
+  repeat do_per_univ_elem_irrel_rewrite1.
+
+Ltac per_univ_elem_irrel_rewrite :=
+  functional_eval_rewrite_clear;
+  do_per_univ_elem_irrel_rewrite;
+  clear_dups.
+
+Lemma per_univ_elem_trans : forall i A1 A2 R,
+    per_univ_elem i A1 A2 R ->
+    forall j A3,
+    per_univ_elem j A2 A3 R ->
+    per_univ_elem i A1 A3 R /\ (forall a1 a2 a3, R a1 a2 -> R a2 a3 -> R a1 a3).
+Proof with solve [mauto].
+  induction 1 using per_univ_elem_ind; intros * HT2;
+    invert_per_univ_elem HT2; clear HT2.
+  - split; mauto.
+    intros * [] [].
+    per_univ_elem_irrel_rewrite.
+    destruct (H1 _ _ _ H0 _ _ H2) as [? ?].
+    econstructor...
+  - split; try econstructor...
+  - per_univ_elem_irrel_rewrite.
+    rename in_rel0 into in_rel.
+    specialize (IHper_univ_elem _ _ equiv_a_a') as [? _].
+    split.
+    + per_univ_elem_econstructor; mauto.
+      intros.
+      assert (equiv_c_c : in_rel c c) by (etransitivity; [ | symmetry]; eassumption).
+      destruct_rel_mod_eval.
+      per_univ_elem_irrel_rewrite.
+      firstorder (econstructor; eauto).
+    + setoid_rewrite H2.
+      intros.
+      assert (equiv_c'_c' : in_rel c' c') by (etransitivity; [symmetry | ]; eassumption).
+      destruct_rel_mod_eval.
+      destruct_rel_mod_app.
+      per_univ_elem_irrel_rewrite.
+      firstorder (econstructor; eauto).
+  - split; try per_univ_elem_econstructor...
+Qed.
+
+Lemma per_univ_elem_cumu : forall {i a0 a1 R},
+    {{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} ->
+    {{ DF a0 ≈ a1 ∈ per_univ_elem (S i) ↘ R }}.
+Proof.
+  simpl.
+  induction 1 using per_univ_elem_ind; subst.
+  - eapply per_univ_elem_core_univ'.
+    lia.
+  - per_univ_elem_econstructor.
+  - per_univ_elem_econstructor; mauto.
+    intros.
+    destruct_rel_mod_eval.
+    econstructor; mauto.
+  - per_univ_elem_econstructor; mauto.
+Qed.
diff --git a/theories/Core/Semantic/PERDefinitions.v b/theories/Core/Semantic/PERDefinitions.v
index e0ac8419..de2e898d 100644
--- a/theories/Core/Semantic/PERDefinitions.v
+++ b/theories/Core/Semantic/PERDefinitions.v
@@ -77,7 +77,9 @@ Inductive per_ne : relation domain :=
 (** Universe/Element PER Definition *)
 
 Section Per_univ_elem_core_def.
-  Variable (i : nat) (per_univ_rec : forall {j}, j < i -> relation domain).
+  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 :
@@ -100,28 +102,20 @@ Section Per_univ_elem_core_def.
   .
 
   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)).
+    (motive : domain -> domain -> relation domain -> Prop)
+      (case_U : forall (j j' : nat) (lt_j_i : j < i), j = j' -> motive d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}} (per_univ_rec lt_j_i))
+      (case_nat : motive d{{{ ℕ }}} d{{{ ℕ }}} per_nat)
+      (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)
+      (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 }} :=
@@ -163,30 +157,22 @@ 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 ->
-        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)).
+    (motive : nat -> domain -> domain -> relation domain -> Prop)
+      (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))
+      (case_N : forall i, motive i d{{{ ℕ }}} d{{{ ℕ }}} per_nat)
+      (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)
+      (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 *.
@@ -225,18 +211,21 @@ Ltac per_univ_elem_econstructor :=
 
 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'.
 
+Definition per_total : relation env := fun p p' => True.
+
 Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
 | per_ctx_env_nil :
-  `{ (Env = fun p p' => True) ->
-     {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ Env }} }
+  `{ {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ per_total }} }
 | per_ctx_env_cons :
   `{ forall (tail_rel : relation env)
-        (head_rel : forall {p p'}, {{ Dom p ≈ p' ∈ tail_rel }} -> relation domain)
+        (head_rel : forall {p p'} (equiv_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 }} }
+        PER 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_rel = 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_rel }} }
 .
 
 Definition per_ctx : relation ctx := fun Γ Γ' => exists R', per_ctx_env Γ Γ' R'.
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index 0448818f..9de240f5 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -1,364 +1,118 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
-From Mcltt Require Import Axioms Base Evaluation LibTactics PERDefinitions Readback.
+From Mcltt Require Import Axioms Base Evaluation LibTactics PERDefinitions PERBasicLemmas Readback Realizability.
 Import Domain_Notations.
 
-(* 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. *)
-
-Lemma per_bot_sym : forall m n,
-    {{ Dom m ≈ n ∈ per_bot }} ->
-    {{ Dom n ≈ m ∈ per_bot }}.
-Proof with solve [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 with solve [mauto].
-  intros * Hmn Hnl s.
-  destruct (Hmn s) as [? []].
-  destruct (Hnl s) as [? []].
-  functional_read_rewrite_clear...
-Qed.
-
-#[export]
-Hint Resolve per_bot_trans : mcltt.
-
-Lemma var_per_bot : forall {n},
-    {{ Dom !n ≈ !n ∈ per_bot }}.
-Proof.
-  intros n s. repeat econstructor.
-Qed.
-
-#[export]
-Hint Resolve var_per_bot : mcltt.
-
-Lemma per_top_sym : forall m n,
-    {{ Dom m ≈ n ∈ per_top }} ->
-    {{ Dom n ≈ m ∈ per_top }}.
-Proof with solve [mauto].
-  intros * H s.
-  destruct (H s) as [? []]...
-Qed.
-
-#[export]
-Hint Resolve per_top_sym : mcltt.
-
-Lemma per_top_trans : forall m n l,
-    {{ Dom m ≈ n ∈ per_top }} ->
-    {{ Dom n ≈ l ∈ per_top }} ->
-    {{ Dom m ≈ l ∈ per_top }}.
-Proof with solve [mauto].
-  intros * Hmn Hnl s.
-  destruct (Hmn s) as [? []].
-  destruct (Hnl s) as [? []].
-  functional_read_rewrite_clear...
-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 }}.
-Proof with solve [mauto].
-  intros * H s.
-  destruct (H s) as [? []]...
-Qed.
-
-#[export]
-Hint Resolve per_top_typ_sym : mcltt.
-
-Lemma per_top_typ_trans : forall m n l,
-    {{ Dom m ≈ n ∈ per_top_typ }} ->
-    {{ Dom n ≈ l ∈ per_top_typ }} ->
-    {{ Dom m ≈ l ∈ per_top_typ }}.
-Proof with solve [mauto].
-  intros * Hmn Hnl s.
-  destruct (Hmn s) as [? []].
-  destruct (Hnl s) as [? []].
-  functional_read_rewrite_clear...
-Qed.
-
-#[export]
-Hint Resolve per_top_typ_trans : mcltt.
-
-Lemma PER_per_top_typ : PER per_top_typ.
-Proof with solve [mauto].
-  econstructor...
-Qed.
-
-Lemma per_nat_sym : forall m n,
-    {{ Dom m ≈ n ∈ per_nat }} ->
-    {{ Dom n ≈ m ∈ per_nat }}.
-Proof with solve [mauto].
-  induction 1; econstructor...
-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 with solve [mauto].
-  intros * H. gen l.
-  induction H; intros * H'; inversion_clear H'; econstructor...
-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 with solve [mauto].
-  intros * [].
-  econstructor...
-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 solve [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'.
+Lemma per_ctx_env_right_irrel : forall Γ Δ Δ' R R',
+    {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ DF Γ ≈ Δ' ∈ per_ctx_env ↘ R' }} ->
+    R = R'.
 Proof.
-  induction 1 using per_univ_elem_ind; intros * Heq Hright;
-    try solve [induction Hright using per_univ_elem_ind; congruence].
+  intros * Horig; gen Δ' R'.
+  induction Horig; intros * Hright;
+    try solve [inversion Hright; congruence].
   subst.
-  invert_per_univ_elem Hright; try congruence.
-  specialize (IHper_univ_elem _ _ _ eq_refl equiv_a_a').
+  inversion_clear Hright.
+  specialize (IHHorig _ _ equiv_Γ_Γ'0).
   subst.
-  extensionality f.
-  extensionality f'.
-  rewrite H2, H10.
-  extensionality c.
-  extensionality c'.
-  extensionality equiv_c_c'.
+  enough (head_rel = head_rel0) by (subst; easy).
+  extensionality p.
+  extensionality p'.
+  extensionality equiv_p_p'.
+  unfold rel_typ in *.
   destruct_rel_mod_eval.
-  functional_eval_rewrite_clear.
-  specialize (H12 _ _ _ eq_refl H5).
+  per_univ_elem_irrel_rewrite.
   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.
-
-Ltac per_univ_elem_right_irrel_rewrite1 :=
-  match goal with
-  | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-      clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
-  end.
-Ltac per_univ_elem_right_irrel_rewrite := repeat per_univ_elem_right_irrel_rewrite1.
-
-Lemma per_univ_elem_sym : forall i A B R,
-    per_univ_elem i A B R ->
-    per_univ_elem i B A R /\ (forall a b, {{ Dom a ≈ b ∈ R }} <-> {{ Dom b ≈ a ∈ R }}).
-Proof.
-  induction 1 using per_univ_elem_ind; subst.
-  - split.
-    + apply per_univ_elem_core_univ'; trivial.
-    + intros. split; intros [].
-      * specialize (H1 _ _ _ H0).
-        firstorder.
-      * specialize (H1 _ _ _ H0).
-        firstorder.
-  - split.
-    + econstructor.
-    + intros; split; mauto.
-  - destruct IHper_univ_elem as [? ?].
-    setoid_rewrite H2.
-    split.
-    + per_univ_elem_econstructor; eauto.
-      intros.
-      assert (equiv_c'_c : in_rel c' c) by firstorder.
-      assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
-      destruct_rel_mod_eval.
-      econstructor; eauto.
-      functional_eval_rewrite_clear.
-      per_univ_elem_right_irrel_rewrite.
-      assumption.
-    + assert (forall a b : domain,
-                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') a c b c') ->
-                 (forall (c c' : domain) (equiv_c_c' : in_rel c c'), rel_mod_app (out_rel c c' equiv_c_c') b c a c')).
-      {
-        intros.
-        assert (equiv_c'_c : in_rel c' c) by firstorder.
-        assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
-        destruct_rel_mod_eval.
-        destruct_rel_mod_app.
-        functional_eval_rewrite_clear.
-        per_univ_elem_right_irrel_rewrite.
-        econstructor; eauto.
-        firstorder.
-      }
-      firstorder.
-  - split.
-    + econstructor; mauto.
-    + intros; split; mauto.
+Lemma per_ctx_env_sym : forall Γ Δ R,
+    {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ DF Δ ≈ Γ ∈ per_ctx_env ↘ R }} /\ (forall o p, {{ Dom o ≈ p ∈ R }} -> {{ Dom p ≈ o ∈ R }}).
+Proof with solve [eauto].
+  simpl.
+  induction 1; firstorder; try solve [econstructor; eauto]; unfold rel_typ in *.
+  - econstructor; eauto; firstorder.
+    assert (tail_rel p' p) by eauto.
+    assert (tail_rel p p) by (etransitivity; eauto).
+    destruct_rel_mod_eval.
+    per_univ_elem_irrel_rewrite.
+    econstructor; eauto.
+    apply per_univ_elem_sym...
+  - subst.
+    firstorder.
+    assert (tail_rel d{{{ p ↯ }}} d{{{ o ↯ }}}) by (unfold Symmetric in *; eauto).
+    assert (tail_rel d{{{ p ↯ }}} d{{{ p ↯ }}}) by (etransitivity; eauto).
+    destruct_rel_mod_eval.
+    eexists.
+    per_univ_elem_irrel_rewrite.
+    eapply per_univ_elem_sym...
 Qed.
 
-Lemma per_univ_elem_left_irrel : forall i A B R A' R',
-    per_univ_elem i A B R ->
-    per_univ_elem i A' B R' ->
+Lemma per_ctx_env_left_irrel : forall Γ Γ' Δ R R',
+    {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ DF Γ' ≈ Δ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
 Proof.
-  intros * []%per_univ_elem_sym []%per_univ_elem_sym.
-  eauto using per_univ_elem_right_irrel.
+  intros * []%per_ctx_env_sym []%per_ctx_env_sym.
+  eauto using per_ctx_env_right_irrel.
 Qed.
 
-Lemma per_univ_elem_cross_irrel : forall i A B R B' R',
-    per_univ_elem i A B R ->
-    per_univ_elem i B' A R' ->
+Lemma per_ctx_env_cross_irrel : forall Γ Δ Δ' R R',
+    {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ DF Δ' ≈ Γ ∈ per_ctx_env ↘ R' }} ->
     R = R'.
 Proof.
-  intros * ? []%per_univ_elem_sym.
-  eauto using per_univ_elem_right_irrel.
+  intros * ? []%per_ctx_env_sym.
+  eauto using per_ctx_env_right_irrel.
 Qed.
 
-Ltac do_per_univ_elem_irrel_rewrite1 :=
+Ltac do_per_ctx_env_irrel_rewrite1 :=
   match goal with
-    | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
-        H2 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by (eauto using per_univ_elem_right_irrel)
-    | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
-        H2 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by (eauto using per_univ_elem_left_irrel)
-    | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
-        H2 : {{ DF ~_ ≈ ~?A ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
+    | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
+        H2 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
+        clean replace R2 with R1 by (eauto using per_ctx_env_right_irrel)
+    | H1 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R1 }},
+        H2 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
+        clean replace R2 with R1 by (eauto using per_ctx_env_left_irrel)
+    | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
+        H2 : {{ DF ~_ ≈ ~?Γ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
         (* Order matters less here as H1 and H2 cannot be exchanged *)
-        clean replace R2 with R1 by (symmetry; eauto using per_univ_elem_cross_irrel)
+        clean replace R2 with R1 by (symmetry; eauto using per_ctx_env_cross_irrel)
     end.
 
-Ltac do_per_univ_elem_irrel_rewrite :=
-  repeat do_per_univ_elem_irrel_rewrite1.
+Ltac do_per_ctx_env_irrel_rewrite :=
+  repeat do_per_ctx_env_irrel_rewrite1.
 
-Ltac per_univ_elem_irrel_rewrite :=
+Ltac per_ctx_env_irrel_rewrite :=
   functional_eval_rewrite_clear;
-  do_per_univ_elem_irrel_rewrite;
+  do_per_ctx_env_irrel_rewrite;
   clear_dups.
 
-Lemma per_univ_elem_trans : forall i A1 A2 R,
-    per_univ_elem i A1 A2 R ->
-    forall A3,
-    per_univ_elem i A2 A3 R ->
-    per_univ_elem i A1 A3 R /\ (forall a1 a2 a3, R a1 a2 -> R a2 a3 -> R a1 a3).
-Proof with solve [mauto].
-  induction 1 using per_univ_elem_ind; intros * HT2;
-    invert_per_univ_elem HT2; clear HT2.
-  - split; mauto.
-    intros * [] [].
-    per_univ_elem_irrel_rewrite.
-    destruct (H1 _ _ _ H0 _ H2) as [? ?].
-    econstructor...
-  - split; try econstructor...
-  - per_univ_elem_irrel_rewrite.
-    rename in_rel0 into in_rel.
-    specialize (IHper_univ_elem _ equiv_a_a') as [? _].
-    split.
-    + per_univ_elem_econstructor; mauto.
-      intros.
-      assert (equiv_c_c : in_rel c c) by (etransitivity; [ | symmetry]; eassumption).
-      destruct_rel_mod_eval.
-      per_univ_elem_irrel_rewrite.
-      firstorder (econstructor; eauto).
-    + setoid_rewrite H2.
+Lemma per_ctx_env_trans : forall Γ1 Γ2 R,
+    {{ DF Γ1 ≈ Γ2 ∈ per_ctx_env ↘ R }} ->
+    forall Γ3,
+      {{ DF Γ2 ≈ Γ3 ∈ per_ctx_env ↘ R }} ->
+      {{ DF Γ1 ≈ Γ3 ∈ per_ctx_env ↘ R }} /\ (forall p1 p2 p3, {{ Dom p1 ≈ p2 ∈ R }} -> {{ Dom p2 ≈ p3 ∈ R }} -> {{ Dom p1 ≈ p3 ∈ R }}).
+Proof with solve [eauto].
+  simpl.
+  induction 1; intros * HTrans23; inversion HTrans23; subst; eauto.
+  per_ctx_env_irrel_rewrite.
+  rename tail_rel0 into tail_rel.
+  split.
+  - econstructor; eauto.
+    + eapply IHper_ctx_env...
+    + unfold rel_typ in *.
       intros.
-      assert (equiv_c'_c' : in_rel c' c') by (etransitivity; [symmetry | ]; eassumption).
+      assert (tail_rel p p) by (etransitivity; [ | symmetry]; eassumption).
       destruct_rel_mod_eval.
-      destruct_rel_mod_app.
+      econstructor; eauto.
       per_univ_elem_irrel_rewrite.
-      firstorder (econstructor; eauto).
-  - split; try per_univ_elem_econstructor...
-Qed.
-
-Lemma per_univ_elem_cumu : forall {i a0 a1 R},
-    {{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} ->
-    {{ DF a0 ≈ a1 ∈ per_univ_elem (S i) ↘ R }}.
-Proof.
-  simpl.
-  induction 1 using per_univ_elem_ind; subst.
-  - eapply per_univ_elem_core_univ'.
-    lia.
-  - per_univ_elem_econstructor.
-  - per_univ_elem_econstructor; mauto.
-    intros.
+      eapply proj1, per_univ_elem_trans; [|eassumption]...
+  - intros * [] [].
+    specialize (IHper_ctx_env _ equiv_Γ_Γ'0) as [].
+    assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by eauto.
+    eexists.
+    unfold rel_typ in *.
     destruct_rel_mod_eval.
-    econstructor; mauto.
-  - per_univ_elem_econstructor; mauto.
+    per_univ_elem_irrel_rewrite.
+    eapply per_univ_elem_trans...
 Qed.
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
index 02f840e6..f0671a15 100644
--- a/theories/Core/Semantic/Realizability.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -1,7 +1,7 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
-From Mcltt Require Import Base Evaluation LibTactics.
-From Mcltt Require Export PER.
+From Mcltt Require Import Base Evaluation LibTactics PERBasicLemmas.
+From Mcltt Require Export PERDefinitions PERBasicLemmas.
 Import Domain_Notations.
 
 Lemma per_nat_then_per_top : forall {n m},
diff --git a/theories/_CoqProject b/theories/_CoqProject
index c714ab5f..7520ea58 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -9,6 +9,7 @@
 ./Core/Semantic/EvaluationDefinitions.v
 ./Core/Semantic/EvaluationLemmas.v
 ./Core/Semantic/PER.v
+./Core/Semantic/PERBasicLemmas.v
 ./Core/Semantic/PERDefinitions.v
 ./Core/Semantic/PERLemmas.v
 ./Core/Semantic/Readback.v