diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v
new file mode 100644
index 00000000..0c857cc8
--- /dev/null
+++ b/theories/Core/Completeness/FunctionCases.v
@@ -0,0 +1,139 @@
+From Coq Require Import Morphisms_Relations RelationClasses SetoidTactics.
+From Mcltt Require Import Base LibTactics LogicalRelation System.
+Import Domain_Notations.
+
+Lemma rel_exp_pi_cong : forall {i Γ A A' B B'},
+  {{ Γ ⊨ A ≈ A' : Type@i }} ->
+  {{ Γ , A ⊨ B ≈ B' : Type@i }} ->
+  {{ Γ ⊨ Π A B ≈ Π A' B' : Type@i }}.
+Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
+  intros * [env_relΓ] [env_relΓA].
+  destruct_conjs.
+  pose (env_relΓ0 := env_relΓ).
+  pose (env_relΓA0 := env_relΓA).
+  inversion_by_head (per_ctx_env env_relΓA); subst.
+  handle_per_ctx_env_irrel.
+  eexists.
+  eexists; [eassumption |].
+  eexists.
+  intros.
+  (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+  rewrite_relation_equivalence_right.
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+  destruct_by_head rel_typ.
+  inversion_by_head (eval_exp {{{ Type@i }}}); subst.
+  match goal with
+  | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
+      invert_per_univ_elem H;
+      apply_relation_equivalence;
+      clear_refl_eqs
+  end.
+  destruct_by_head rel_exp.
+  destruct_conjs.
+  handle_per_univ_elem_irrel.
+  exists (per_univ i).
+  split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
+  unfold per_univ.
+  eexists.
+  per_univ_elem_econstructor; try (now eauto); try setoid_reflexivity.
+  - eauto with typeclass_instances.
+  - instantiate (1 := fun c c' (equiv_c_c' : head_rel p p' equiv_p_p' c c') b b' =>
+                        forall a a' R,
+                          {{ ⟦ B ⟧ p ↦ c ↘ a }} ->
+                          {{ ⟦ B' ⟧ p' ↦ c' ↘ a' }} ->
+                          per_univ_elem i R a a' -> R b b').
+    intros.
+    assert (equiv_pc_p'c' : {{ Dom p ↦ c ≈ p' ↦ c' ∈ env_relΓA }}) by (apply_relation_equivalence; eexists; eauto).
+    apply_relation_equivalence.
+    (on_all_hyp: fun H => destruct (H _ _ equiv_pc_p'c') as [? []]).
+    destruct_by_head rel_typ.
+    destruct_by_head rel_exp.
+    inversion_by_head (eval_exp {{{ Type@i }}}).
+    subst.
+    match goal with
+    | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
+        invert_per_univ_elem H;
+        apply_relation_equivalence;
+        clear_refl_eqs
+    end.
+    destruct_conjs.
+    econstructor; mauto.
+    evar (elem_rel : relation domain).
+    match goal with
+    | |- per_univ_elem _ ?R _ _ => setoid_replace R with elem_rel; subst elem_rel; [eassumption |]
+    end.
+    split; intros; handle_per_univ_elem_irrel; intuition.
+  - match goal with
+    | |- ?X <~> ?Y => instantiate (1 := Y)
+    end.
+    reflexivity.
+Qed.      
+
+Lemma rel_exp_pi_sub : forall {i Γ σ Δ A B},
+    {{ Γ ⊨s σ : Δ }} ->
+    {{ Δ ⊨ A : Type@i }} ->
+    {{ Δ , A ⊨ B : Type@i }} ->
+    {{ Γ ⊨ (Π A B)[σ] ≈ Π (A[σ]) (B[q σ]) : Type@i }}.
+Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
+  intros * [env_relΓ] [] [env_relΔA].
+  destruct_conjs.
+  pose (env_relΔA0 := env_relΔA).
+  inversion_by_head (per_ctx_env env_relΔA); subst.
+  handle_per_ctx_env_irrel.
+  eexists.
+  eexists; [eassumption |].
+  eexists.
+  intros.
+  (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
+  (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
+  destruct_by_head rel_typ.
+  inversion_by_head (eval_exp {{{ Type@i }}}); subst.
+  match goal with
+  | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
+      invert_per_univ_elem H;
+      apply_relation_equivalence;
+      clear_refl_eqs
+  end.
+  destruct_by_head rel_exp.
+  destruct_conjs.
+  handle_per_univ_elem_irrel.
+  eexists; split;
+    [> econstructor; only 1-2: repeat econstructor; eauto ..].
+  eexists.
+  per_univ_elem_econstructor; eauto with typeclass_instances.
+  - instantiate (1 := fun c c' (equiv_c_c' : head_rel o o' H9 c c') b b' =>
+                        forall a a' R,
+                          {{ ⟦ B ⟧ o ↦ c ↘ a }} ->
+                          {{ ⟦ B[q σ] ⟧ p' ↦ c' ↘ a' }} ->
+                          per_univ_elem i R a a' -> R b b').
+    intros.
+    assert (equiv_pc_p'c' : {{ Dom o ↦ c ≈ o' ↦ c' ∈ env_relΔA }}) by (apply_relation_equivalence; eexists; eauto).
+    apply_relation_equivalence.
+    (on_all_hyp: fun H => destruct (H _ _ equiv_pc_p'c') as [? []]).
+    destruct_by_head rel_typ.
+    inversion_by_head (eval_exp {{{ Type@i }}}); subst.
+    match goal with
+    | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
+        invert_per_univ_elem H;
+        apply_relation_equivalence;
+        clear_refl_eqs
+    end.
+    destruct_by_head rel_exp.
+    destruct_conjs.
+    econstructor; only 1-2: repeat econstructor; eauto.
+    evar (elem_rel : relation domain).
+    match goal with
+    | |- per_univ_elem _ ?R _ _ => setoid_replace R with elem_rel; subst elem_rel; [eassumption |]
+    end.
+    split; intros; handle_per_univ_elem_irrel; intuition.
+    enough {{ ⟦ B[q σ] ⟧ p' ↦ c' ↘ m' }} by intuition.
+    repeat econstructor; eauto.
+  - match goal with
+    | |- ?X <~> ?Y => instantiate (1 := Y)
+    end.
+    reflexivity.
+Qed.
diff --git a/theories/Core/Completeness/LogicalRelation.v b/theories/Core/Completeness/LogicalRelation.v
index c71c7c24..5c8daddf 100644
--- a/theories/Core/Completeness/LogicalRelation.v
+++ b/theories/Core/Completeness/LogicalRelation.v
@@ -1,41 +1 @@
-From Coq Require Import Relations.
-From Mcltt Require Import Base.
-From Mcltt Require Export Evaluation PER.
-Import Domain_Notations.
-
-Inductive rel_exp (R : relation domain) M p M' p' : Prop :=
-| mk_rel_exp : forall m m', {{ ⟦ M ⟧ p ↘ m }} -> {{ ⟦ M' ⟧ p' ↘ m' }} -> {{ Dom m ≈ m' ∈ R }} -> rel_exp R M p M' p'.
-#[global]
-Arguments mk_rel_exp {_ _ _ _ _}.
-
-Definition rel_exp_under_ctx Γ M M' A :=
-  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
-  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
-  exists (elem_rel : relation domain),
-     rel_typ i A p A p' elem_rel /\ rel_exp elem_rel M p M' p'.
-
-Definition valid_exp_under_ctx Γ M A := rel_exp_under_ctx Γ M M A.
-#[global]
-Arguments valid_exp_under_ctx _ _ _ /.
-
-Inductive rel_subst (R : relation env) σ p σ' p' : Prop :=
-| mk_rel_subst : forall o o', {{ ⟦ σ ⟧s p ↘ o }} -> {{ ⟦ σ' ⟧s p' ↘ o' }} -> {{ Dom o ≈ o' ∈ R }} -> rel_subst R σ p σ' p'.
-#[global]
-Arguments mk_rel_subst {_ _ _ _ _ _}.
-
-Definition rel_subst_under_ctx Γ σ σ' Δ :=
-  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }})
-     env_rel' (_ : {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ env_rel' }}),
-  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
-    rel_subst env_rel' σ p σ' p'.
-
-Definition valid_subst_under_ctx Γ σ Δ := rel_subst_under_ctx Γ σ σ Δ.
-#[global]
-Arguments valid_subst_under_ctx _ _ _ /.
-
-Notation "⊨ Γ ≈ Γ'" := (per_ctx Γ Γ')  (in custom judg at level 80, Γ custom exp, Γ' custom exp).
-Notation "⊨ Γ" := (valid_ctx Γ) (in custom judg at level 80, Γ custom exp).
-Notation "Γ ⊨ M ≈ M' : A" := (rel_exp_under_ctx Γ M M' A) (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
-Notation "Γ ⊨ M : A" := (valid_exp_under_ctx Γ M A) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
-Notation "Γ ⊨s σ ≈ σ' : Δ" := (rel_subst_under_ctx Γ σ σ' Δ) (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
-Notation "Γ ⊨s σ : Δ" := (valid_subst_under_ctx Γ σ Δ) (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).
+From Mcltt.Core.Completeness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas.
diff --git a/theories/Core/Completeness/LogicalRelation/Definitions.v b/theories/Core/Completeness/LogicalRelation/Definitions.v
new file mode 100644
index 00000000..d67b6a92
--- /dev/null
+++ b/theories/Core/Completeness/LogicalRelation/Definitions.v
@@ -0,0 +1,41 @@
+From Coq Require Import Relations.
+From Mcltt Require Import Base.
+From Mcltt Require Export Evaluation PER.
+Import Domain_Notations.
+
+Inductive rel_exp M p M' p' (R : relation domain) : Prop :=
+| mk_rel_exp : forall m m', {{ ⟦ M ⟧ p ↘ m }} -> {{ ⟦ M' ⟧ p' ↘ m' }} -> {{ Dom m ≈ m' ∈ R }} -> rel_exp M p M' p' R.
+#[global]
+Arguments mk_rel_exp {_ _ _ _ _}.
+
+Definition rel_exp_under_ctx Γ M M' A :=
+  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }}) i,
+  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+  exists (elem_rel : relation domain),
+     rel_typ i A p A p' elem_rel /\ rel_exp M p M' p' elem_rel.
+
+Definition valid_exp_under_ctx Γ M A := rel_exp_under_ctx Γ M M A.
+#[global]
+Arguments valid_exp_under_ctx _ _ _ /.
+
+Inductive rel_subst σ p σ' p' (R : relation env) : Prop :=
+| mk_rel_subst : forall o o', {{ ⟦ σ ⟧s p ↘ o }} -> {{ ⟦ σ' ⟧s p' ↘ o' }} -> {{ Dom o ≈ o' ∈ R }} -> rel_subst σ p σ' p' R.
+#[global]
+Arguments mk_rel_subst {_ _ _ _ _ _}.
+
+Definition rel_subst_under_ctx Γ σ σ' Δ :=
+  exists env_rel (_ : {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }})
+     env_rel' (_ : {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ env_rel' }}),
+  forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
+    rel_subst σ p σ' p' env_rel'.
+
+Definition valid_subst_under_ctx Γ σ Δ := rel_subst_under_ctx Γ σ σ Δ.
+#[global]
+Arguments valid_subst_under_ctx _ _ _ /.
+
+Notation "⊨ Γ ≈ Γ'" := (per_ctx Γ Γ')  (in custom judg at level 80, Γ custom exp, Γ' custom exp).
+Notation "⊨ Γ" := (valid_ctx Γ) (in custom judg at level 80, Γ custom exp).
+Notation "Γ ⊨ M ≈ M' : A" := (rel_exp_under_ctx Γ M M' A) (in custom judg at level 80, Γ custom exp, M custom exp, M' custom exp, A custom exp).
+Notation "Γ ⊨ M : A" := (valid_exp_under_ctx Γ M A) (in custom judg at level 80, Γ custom exp, M custom exp, A custom exp).
+Notation "Γ ⊨s σ ≈ σ' : Δ" := (rel_subst_under_ctx Γ σ σ' Δ) (in custom judg at level 80, Γ custom exp, σ custom exp, σ' custom exp, Δ custom exp).
+Notation "Γ ⊨s σ : Δ" := (valid_subst_under_ctx Γ σ Δ) (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).
diff --git a/theories/Core/Completeness/LogicalRelation/Lemmas.v b/theories/Core/Completeness/LogicalRelation/Lemmas.v
new file mode 100644
index 00000000..dc2dd3a1
--- /dev/null
+++ b/theories/Core/Completeness/LogicalRelation/Lemmas.v
@@ -0,0 +1,20 @@
+From Coq Require Import Morphisms Morphisms_Relations RelationClasses.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Completeness Require Import LogicalRelation.Definitions.
+Import Domain_Notations.
+
+Add Parametric Morphism M p M' p' : (rel_exp M p M' p')
+    with signature (@relation_equivalence domain) ==> iff as rel_exp_morphism.
+Proof.
+  intros R R' HRR'.
+  split; intros []; econstructor; eauto;
+    apply HRR'; eassumption.
+Qed.
+
+Add Parametric Morphism σ p σ' p' : (rel_subst σ p σ' p')
+    with signature (@relation_equivalence env) ==> iff as rel_subst_morphism.
+Proof.
+  intros R R' HRR'.
+  split; intros []; econstructor; eauto;
+    apply HRR'; eassumption.
+Qed.
diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v
index 28231956..ef146323 100644
--- a/theories/Core/Completeness/TermStructureCases.v
+++ b/theories/Core/Completeness/TermStructureCases.v
@@ -1,4 +1,4 @@
-From Coq Require Import Relations RelationClasses.
+From Coq Require Import Morphisms_Relations RelationClasses.
 From Mcltt Require Import Base LibTactics LogicalRelation System.
 Import Domain_Notations.
 
@@ -7,22 +7,25 @@ Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
     {{ Γ ⊨s σ ≈ σ' : Δ }} ->
     {{ Γ ⊨ M[σ] ≈ M'[σ'] : A[σ] }}.
 Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΔ] [env_relΓ].
   destruct_conjs.
-  per_ctx_env_irrel_rewrite.
+  pose (env_relΔ0 := env_relΔ).
+  handle_per_ctx_env_irrel.
   eexists.
   eexists; try eassumption.
   eexists.
   intros.
-  assert (env_relΓ p' p) by (eapply per_env_sym; eauto).
-  assert (env_relΓ p p) by (eapply per_env_trans; eauto).
+  assert (env_relΓ p' p) by (symmetry; eauto).
+  assert (env_relΓ p p) by (etransitivity; eauto).
   (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
-  per_univ_elem_irrel_rewrite.
-  assert (env_relΔ o o0) by (eapply per_env_trans; [eauto | | eapply per_env_sym]; revgoals; eauto).
+  handle_per_univ_elem_irrel.
+  assert (env_relΔ o o0) by (etransitivity; [|symmetry; intuition]; intuition).
   (on_all_hyp: fun H => destruct_rel_by_assumption env_relΔ H).
   destruct_by_head rel_exp.
   destruct_by_head rel_typ.
-  per_univ_elem_irrel_rewrite.
+  handle_per_univ_elem_irrel.
   eexists.
   split; [> econstructor; only 1-2: econstructor; eauto ..].
 Qed.
@@ -51,9 +54,13 @@ Lemma rel_exp_sub_compose : forall {Γ τ Γ' σ Γ'' M A},
     {{ Γ'' ⊨ M : A }} ->
     {{ Γ ⊨ M[σ ∘ τ] ≈ M[σ][τ] : A[σ ∘ τ] }}.
 Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΓ [? [env_relΓ']]] [? [? [env_relΓ'']]] [].
   destruct_conjs.
-  per_ctx_env_irrel_rewrite.
+  pose (env_relΓ'0 := env_relΓ').
+  pose (env_relΓ''0 := env_relΓ'').
+  handle_per_ctx_env_irrel.
   eexists.
   eexists; try eassumption.
   eexists.
@@ -61,15 +68,16 @@ Proof.
   assert (env_relΓ p' p) by (eapply per_env_sym; eauto).
   assert (env_relΓ p p) by (eapply per_env_trans; eauto).
   (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H).
-  per_univ_elem_irrel_rewrite.
+  handle_per_univ_elem_irrel.
   (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ' H).
-  per_univ_elem_irrel_rewrite.
+  handle_per_univ_elem_irrel.
   (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ'' H).
+  handle_per_univ_elem_irrel.
   destruct_by_head rel_exp.
   destruct_by_head rel_typ.
-  per_univ_elem_irrel_rewrite.
+  handle_per_univ_elem_irrel.
   eexists.
-  split; [> econstructor; only 1-2: repeat econstructor; mauto ..].
+  split; [> econstructor; only 1-2: repeat econstructor; eauto ..].
 Qed.
 
 Lemma rel_exp_conv : forall {Γ M M' A A' i},
@@ -77,9 +85,12 @@ Lemma rel_exp_conv : forall {Γ M M' A A' i},
     {{ Γ ⊨ A ≈ A' : Type@i }} ->
     {{ Γ ⊨ M ≈ M' : A' }}.
 Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΓ] [env_relΓ'].
   destruct_conjs.
-  per_ctx_env_irrel_rewrite.
+  pose (env_relΓ0 := env_relΓ).
+  handle_per_ctx_env_irrel.
   eexists.
   eexists; try eassumption.
   eexists.
@@ -89,19 +100,26 @@ Proof.
   destruct_by_head rel_exp.
   destruct_by_head rel_typ.
   inversion_by_head (eval_exp {{{ Type@i }}}); subst.
-  per_univ_elem_irrel_rewrite.
-  match_by_head1 per_univ_elem ltac:(fun H => invert_per_univ_elem H; let n := numgoals in guard n <= 1); clear_refl_eqs.
+  handle_per_univ_elem_irrel.
+  match goal with
+  | H : per_univ_elem _ _ d{{{ 𝕌@?i }}} d{{{ 𝕌@?i }}} |- _ =>
+      invert_per_univ_elem H;
+      apply_relation_equivalence;
+      clear_refl_eqs
+  end.
   destruct_conjs.
-  per_univ_elem_irrel_rewrite.
+  handle_per_univ_elem_irrel.
   eexists.
   split; econstructor; eauto.
-  eapply per_univ_trans; [eapply per_univ_sym |]; eauto.
+  etransitivity; [symmetry |]; eauto.
 Qed.
 
 Lemma rel_exp_sym : forall {Γ M M' A},
     {{ Γ ⊨ M ≈ M' : A }} ->
     {{ Γ ⊨ M' ≈ M : A }}.
 Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΓ].
   destruct_conjs.
   econstructor.
@@ -112,7 +130,7 @@ Proof.
   (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H); destruct_conjs.
   destruct_by_head rel_exp.
   destruct_by_head rel_typ.
-  per_univ_elem_irrel_rewrite.
+  handle_per_univ_elem_irrel.
   eexists.
   split; econstructor; eauto.
   eapply per_elem_sym; eauto.
@@ -123,20 +141,23 @@ Lemma rel_exp_trans : forall {Γ M1 M2 M3 A},
     {{ Γ ⊨ M2 ≈ M3 : A }} ->
     {{ Γ ⊨ M1 ≈ M3 : A }}.
 Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
   intros * [env_relΓ] [env_relΓ'].
   destruct_conjs.
-  per_ctx_env_irrel_rewrite.
+  pose (env_relΓ0 := env_relΓ).
+  handle_per_ctx_env_irrel.
   econstructor.
   eexists; try eassumption.
   eexists.
   intros ? ? equiv_p_p'.
-  assert (env_relΓ p' p) by (eapply per_env_sym; eauto).
-  assert (env_relΓ p' p') by (eapply per_env_trans; eauto).
+  assert (env_relΓ p' p) by (symmetry; eauto).
+  assert (env_relΓ p' p') by (etransitivity; eauto).
   (on_all_hyp: fun H => destruct_rel_by_assumption env_relΓ H); destruct_conjs.
   destruct_by_head rel_exp.
   destruct_by_head rel_typ.
-  per_univ_elem_irrel_rewrite.
+  handle_per_univ_elem_irrel.
   eexists.
   split; econstructor; eauto.
-  eapply per_elem_trans; eauto.
+  etransitivity; eauto.
 Qed.
diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v
index 9e4af774..6b55077c 100644
--- a/theories/Core/Completeness/UniverseCases.v
+++ b/theories/Core/Completeness/UniverseCases.v
@@ -1,3 +1,4 @@
+From Coq Require Import Morphisms_Relations.
 From Mcltt Require Import Base LibTactics LogicalRelation.
 Import Domain_Notations.
 
@@ -11,7 +12,8 @@ Proof.
   eexists.
   intros.
   exists (per_univ (S i)).
-  unshelve (split; repeat econstructor); mauto.
+  split; [> econstructor; only 1-2: econstructor; eauto ..]; [| exists (per_univ i)];
+    per_univ_elem_econstructor; mauto; reflexivity.
 Qed.
 
 Lemma rel_exp_typ_sub : forall {i Γ σ Δ},
@@ -26,13 +28,16 @@ Proof.
   intros.
   exists (per_univ (S i)).
   (on_all_hyp: fun H => destruct_rel_by_assumption env_rel H).
-  unshelve (split; repeat econstructor); only 4: eauto; mauto.
+  split; [> econstructor; only 1-2: repeat econstructor; eauto ..]; [| exists (per_univ i)];
+    per_univ_elem_econstructor; mauto; reflexivity.
 Qed.
 
 Lemma rel_exp_cumu : forall {i Γ A A'},
     {{ Γ ⊨ A ≈ A' : Type@i }} ->
     {{ Γ ⊨ A ≈ A' : Type@(S i) }}.
 Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
   intros * [env_rel].
   destruct_conjs.
   econstructor.
@@ -45,8 +50,10 @@ Proof.
   inversion_by_head rel_exp.
   inversion_by_head (eval_exp {{{ Type@i }}}); subst.
   match_by_head per_univ_elem ltac:(fun H => invert_per_univ_elem H); subst.
+  handle_per_univ_elem_irrel.
   destruct_conjs.
-  per_univ_elem_irrel_rewrite.
   match_by_head per_univ_elem ltac:(fun H => apply per_univ_elem_cumu in H).
-  split; econstructor; try eassumption; repeat econstructor; mauto.
+  split; [> econstructor; only 1-2: repeat econstructor; eauto ..]; [| eexists; eauto].
+  per_univ_elem_econstructor; mauto.
+  reflexivity.
 Qed.
diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v
index d2e1c72e..3d3d04e8 100644
--- a/theories/Core/Completeness/VariableCases.v
+++ b/theories/Core/Completeness/VariableCases.v
@@ -1,4 +1,4 @@
-From Coq Require Import Relations.
+From Coq Require Import Morphisms_Relations Relations.
 From Mcltt Require Import Base LibTactics LogicalRelation System.
 Import Domain_Notations.
 
@@ -8,15 +8,18 @@ Lemma valid_lookup : forall {Γ x A env_rel}
     exists i,
     forall p p' (equiv_p_p' : {{ Dom p ≈ p' ∈ env_rel }}),
     exists elem_rel,
-      rel_typ i A p A p' elem_rel /\ rel_exp elem_rel {{{ #x }}} p {{{ #x }}} p'.
+      rel_typ i A p A p' elem_rel /\ rel_exp {{{ #x }}} p {{{ #x }}} p' elem_rel.
 Proof with solve [repeat econstructor; mauto].
-  intros.
-  assert {{ #x : A ∈ Γ }} as HxinΓ by mauto.
-  remember Γ as Δ eqn:HΔΓ in HxinΓ, equiv_Γ_Γ at 2. clear HΔΓ. rename equiv_Γ_Γ into equiv_Γ_Δ.
-  remember A as A' eqn:HAA' in HxinΓ |- * at 2. clear HAA'.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
+  intros * ? HxinΓ.
+  assert {{ #x : A ∈ Γ }} as HxinΓ' by mauto.
+  remember Γ as Δ eqn:HΔΓ in HxinΓ', equiv_Γ_Γ at 2. clear HΔΓ. rename equiv_Γ_Γ into equiv_Γ_Δ.
+  remember A as A' eqn:HAA' in HxinΓ' |- * at 2. clear HAA'.
   gen Δ A' env_rel.
-  induction H; intros * equiv_Γ_Δ H0; inversion H0; subst; clear H0; inversion_clear equiv_Γ_Δ; subst;
-    try (specialize (IHctx_lookup _ _ _ equiv_Γ_Γ' H2) as [j ?]; destruct_conjs);
+  induction HxinΓ; intros * equiv_Γ_Δ HxinΓ0; inversion HxinΓ0; subst; clear HxinΓ0; inversion_clear equiv_Γ_Δ; subst;
+    [|specialize (IHHxinΓ _ _ _ equiv_Γ_Γ' H2) as [j ?]; destruct_conjs];
+    apply_relation_equivalence;
     eexists; intros ? ? [];
     (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H); destruct_conjs;
     eexists.
@@ -42,6 +45,8 @@ Lemma rel_exp_var_weaken : forall {Γ B x A},
     {{ #x : A ∈ Γ }} ->
     {{ Γ , B ⊨ #x[Wk] ≈ #(S x) : A[Wk] }}.
 Proof.
+  pose proof (@relation_equivalence_pointwise domain).
+  pose proof (@relation_equivalence_pointwise env).
   intros * [] HxinΓ.
   match_by_head1 per_ctx_env ltac:(fun H => inversion H); subst.
   unshelve epose proof (valid_lookup _ HxinΓ); revgoals; mauto.
@@ -49,6 +54,7 @@ Proof.
   eexists.
   eexists; try eassumption.
   eexists.
+  apply_relation_equivalence.
   intros ? ? [].
   (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
   destruct_by_head rel_typ.
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index 3547a029..59d8fde5 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -1 +1 @@
-From Mcltt Require Export PER.Definitions PER.Lemmas.
+From Mcltt Require Export PER.Definitions PER.Lemmas PER.CoreTactics.
diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
new file mode 100644
index 00000000..4a9f1ce2
--- /dev/null
+++ b/theories/Core/Semantic/PER/CoreTactics.v
@@ -0,0 +1,48 @@
+From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
+From Equations Require Import Equations.
+From Mcltt Require Import Base Evaluation LibTactics PER.Definitions Readback.
+Import Domain_Notations.
+
+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.
+Ltac destruct_rel_typ :=
+  repeat
+    match goal with
+    | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_typ _ _ _ _ _ _) |- _ =>
+        destruct_rel_by_assumption in_rel H; mark H
+    end;
+  unmark_all.
+
+(** 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 *.
diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v
index a7e1704f..cb071cd0 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -8,42 +8,25 @@ Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at lev
 Notation "'DF' a ≈ b ∈ R ↘ R'" := ((R R' a b : 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 R' a b : (Prop : Type)) (in custom judg at level 90, a custom exp, b custom exp, R constr, R' constr).
+(* Precedences of the next notations follow the ones in the standard library.
+   However, we do not use the ones in the standard library so that we can change
+   the relation if necessary in the future. *)
+Notation "R ~> R'" := (subrelation R R') (at level 70, right associativity).
+Notation "R <~> R'" := (relation_equivalence R R') (at level 95, no associativity).
 
 Generalizable All Variables.
 
 (** Helper Bundles *)
+(* Related modulo evaluation *)
 Inductive rel_mod_eval (R : relation domain -> domain -> 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'.
+(* Related modulo application *)
+Inductive rel_mod_app f a f' a' (R : relation domain) : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app f a f' a' R.
 #[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 }}).
@@ -83,56 +66,74 @@ Section Per_univ_elem_core_def.
 
   Inductive per_univ_elem_core : relation domain -> domain -> domain -> Prop :=
   | per_univ_elem_core_univ :
-    `{ forall (lt_j_i : j < i),
+    `{ forall (elem_rel : relation domain)
+          (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 }}
+          (elem_rel <~> per_univ_rec lt_j_i) ->
+          {{ DF 𝕌@j ≈ 𝕌@j' ∈ per_univ_elem_core ↘ elem_rel }} }
+  | per_univ_elem_core_nat :
+    forall (elem_rel : relation domain),
+      (elem_rel <~> per_nat) ->
+      {{ DF ℕ ≈ ℕ ∈ per_univ_elem_core ↘ elem_rel }}
   | 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)
+         (elem_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') ->
+          (elem_rel <~> fun f f' => forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app f c f' c' (out_rel equiv_c_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 }} }
+    `{ forall (elem_rel : relation domain),
+          {{ Dom b ≈ b' ∈ per_bot }} ->
+          (elem_rel <~> per_ne) ->
+          {{ DF ⇑ a b ≈ ⇑ a' b' ∈ per_univ_elem_core ↘ elem_rel }} }
   .
 
   Hypothesis
     (motive : relation domain -> domain -> domain -> Prop)
-      (case_U : forall (j j' : nat) (lt_j_i : j < i), j = j' -> motive (per_univ_rec lt_j_i) d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
-      (case_nat : motive per_nat d{{{ ℕ }}} d{{{ ℕ }}})
+      (case_U : forall {j j' elem_rel} (lt_j_i : j < i),
+          j = j' ->
+          (elem_rel <~> per_univ_rec lt_j_i) ->
+          motive elem_rel d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
+      (case_nat : forall {elem_rel},
+          (elem_rel <~> per_nat) ->
+          motive elem_rel d{{{ ℕ }}} d{{{ ℕ }}})
       (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),
+        forall {A p B A' p' B' in_rel}
+           (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
+           {elem_rel},
           {{ DF A ≈ A' ∈ per_univ_elem_core ↘ in_rel }} ->
           motive in_rel A A' ->
           PER in_rel ->
           (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
               rel_mod_eval (fun R x y => {{ DF x ≈ y ∈ per_univ_elem_core ↘ R }} /\ motive R x y) 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') ->
+          (elem_rel <~> fun f f' => forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app f c f' c' (out_rel equiv_c_c')) ->
           motive elem_rel d{{{ Π A p B }}} d{{{ Π A' p' B' }}})
-      (case_ne : (forall {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive per_ne d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}})).
+      (case_ne : forall {a b a' b' elem_rel},
+          {{ Dom b ≈ b' ∈ per_bot }} ->
+          (elem_rel <~> per_ne) ->
+          motive elem_rel d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}}).
 
   #[derive(equations=no, eliminator=no)]
   Equations per_univ_elem_core_strong_ind R a b (H : {{ DF a ≈ b ∈ per_univ_elem_core ↘ R }}) : {{ DF a ≈ b ∈ motive ↘ R }} :=
-  | R, a, b, (per_univ_elem_core_univ lt_j_i eq)                         => case_U _ _ lt_j_i eq;
-  | R, a, b, per_univ_elem_core_nat                                      => case_nat;
-  | R, a, b, (per_univ_elem_core_pi in_rel out_rel equiv_a_a' per HT HE) =>
+  | R, a, b, (per_univ_elem_core_univ _ lt_j_i HE eq)                 => case_U lt_j_i HE eq;
+  | R, a, b, (per_univ_elem_core_nat _ HE)                            => case_nat HE;
+  | R, a, b, (per_univ_elem_core_pi _ 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;
-  | R, a, b, (per_univ_elem_core_neut equiv_b_b')                        => case_ne equiv_b_b'.
+  | R, a, b, (per_univ_elem_core_neut _ equiv_b_b' HE)                => case_ne equiv_b_b' HE.
 
 End Per_univ_elem_core_def.
 
-Global Hint Constructors per_univ_elem_core : mcltt.
+#[export]
+Hint Constructors per_univ_elem_core : mcltt.
 
 Equations per_univ_elem (i : nat) : relation domain -> domain -> 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' }}).
@@ -141,38 +142,47 @@ Definition per_univ (i : nat) : relation domain := fun a a' => exists R', {{ DF
 #[global]
 Arguments per_univ _ _ _ /.
 
-Lemma per_univ_elem_core_univ' : forall j i,
+Lemma per_univ_elem_core_univ' : forall j i elem_rel,
     j < i ->
-    {{ DF 𝕌@j ≈ 𝕌@j ∈ per_univ_elem i ↘ per_univ j }}.
+    (elem_rel <~> per_univ j) ->
+    {{ DF 𝕌@j ≈ 𝕌@j ∈ per_univ_elem i ↘ elem_rel }}.
 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).
+  apply per_univ_elem_core_univ; try assumption.
   reflexivity.
 Qed.
-Global Hint Resolve per_univ_elem_core_univ' : mcltt.
+#[export]
+Hint Resolve per_univ_elem_core_univ' : mcltt.
 
 (** Universe/Element PER Induction Principle *)
 
 Section Per_univ_elem_ind_def.
   Hypothesis
     (motive : nat -> relation domain -> domain -> 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 R A B) ->
-                           motive i (per_univ j) d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
-      (case_N : forall i, motive i per_nat d{{{ ℕ }}} d{{{ ℕ }}})
+      (case_U : forall i {j j' elem_rel},
+          j < i -> j = j' ->
+          (elem_rel <~> per_univ j) ->
+          (forall A B R, {{ DF A ≈ B ∈ per_univ_elem j ↘ R }} -> motive j R A B) ->
+          motive i elem_rel d{{{ 𝕌@j }}} d{{{ 𝕌@j' }}})
+      (case_N : forall i {elem_rel},
+          (elem_rel <~> per_nat) ->
+          motive i elem_rel d{{{ ℕ }}} d{{{ ℕ }}})
       (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),
+        forall i {A p B A' p' B' in_rel}
+           (out_rel : forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), relation domain)
+           {elem_rel},
           {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel }} ->
           motive i in_rel A A' ->
           PER in_rel ->
           (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
               rel_mod_eval (fun R x y => {{ DF x ≈ y ∈ per_univ_elem i ↘ R }} /\ motive i R x y) 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') ->
+          (elem_rel <~> fun f f' => forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app f c f' c' (out_rel equiv_c_c')) ->
           motive i elem_rel d{{{ Π A p B }}} d{{{ Π A' p' B' }}})
-      (case_ne : (forall i {a b a' b'}, {{ Dom b ≈ b' ∈ per_bot }} -> motive i per_ne d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}})).
+      (case_ne : forall i {a b a' b' elem_rel},
+          {{ Dom b ≈ b' ∈ per_bot }} ->
+          (elem_rel <~> per_ne) ->
+          motive i elem_rel d{{{ ⇑ a b }}} d{{{ ⇑ a' b' }}}).
 
   #[local]
   Ltac def_simp := simp per_univ_elem in *.
@@ -182,50 +192,38 @@ Section Per_univ_elem_ind_def.
     (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, R, a, b, 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' _ R' A B _))
-        (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)
+        (fun _ _ _ j_lt_i eq HE => case_U i j_lt_i eq HE (fun A B R' H' => per_univ_elem_ind' _ R' A B _))
+        (fun _ => case_N i)
+        (fun _ _ _ _ _ _ _ out_rel _ _ IHA per _ => case_Pi i out_rel _ IHA per _)
+        (fun _ _ _ _ _ => case_ne i)
         R a b 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'.
 Arguments rel_typ _ _ _ _ _ _ /.
 
-Definition per_total : relation env := fun p p' => True.
-
 Inductive per_ctx_env : relation env -> ctx -> ctx -> Prop :=
 | per_ctx_env_nil :
-  `{ {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ per_total }} }
+  `{ forall env_rel,
+        (env_rel <~> fun p p' => True) ->
+        {{ EF ⋅ ≈ ⋅ ∈ per_ctx_env ↘ env_rel }} }
 | per_ctx_env_cons :
-  `{ forall (tail_rel : relation env)
+  `{ forall tail_rel
         (head_rel : forall {p p'} (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}), relation domain)
+        env_rel
         (equiv_Γ_Γ' : {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ tail_rel }}),
         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 }}) ->
+        (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 }} }
 .
 
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index fde056cc..c028748c 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -1,8 +1,36 @@
-From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
+From Coq Require Import Lia Morphisms Morphisms_Prop Morphisms_Relations PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
-From Mcltt Require Import Axioms Base Evaluation LibTactics PER.Definitions Readback.
+From Mcltt Require Import Base Evaluation LibTactics PER.Definitions PER.CoreTactics Readback.
 Import Domain_Notations.
 
+Add Parametric Morphism A : (@all A)
+    with signature forall_relation (fun (x : A) => iff) ==> iff as all_iff_moprhism'.
+Proof.
+  unfold forall_relation.
+  split; intros ** ?; intuition.
+Qed.
+
+Add Parametric Morphism A : PER
+    with signature (@relation_equivalence A) ==> iff as PER_morphism.
+Proof.
+  split; intros []; econstructor; unfold Symmetric, Transitive in *; intuition.
+Qed.
+
+Add Parametric Morphism R0 `(R0_morphism : Proper _ ((@relation_equivalence domain) ==> (@relation_equivalence domain)) R0) A p A' p' : (rel_mod_eval R0 A p A' p')
+    with signature (@relation_equivalence domain) ==> iff as rel_mod_eval_morphism.
+Proof.
+  split; intros []; econstructor; try eassumption;
+    [> eapply R0_morphism; [symmetry + idtac |]; eassumption ..].
+Qed.
+
+Add Parametric Morphism f a f' a' : (rel_mod_app f a f' a')
+    with signature (@relation_equivalence domain) ==> iff as rel_mod_app_morphism.
+Proof.
+  intros * HRR'.
+  split; intros []; econstructor; try eassumption;
+    apply HRR'; eassumption.
+Qed.
+
 Lemma per_bot_sym : forall m n,
     {{ Dom m ≈ n ∈ per_bot }} ->
     {{ Dom n ≈ m ∈ per_bot }}.
@@ -149,53 +177,118 @@ Qed.
 #[export]
 Hint Resolve per_ne_trans : mcltt.
 
-Lemma per_univ_elem_right_irrel : forall i i' R A B R' B',
-    per_univ_elem i R A B ->
-    per_univ_elem i' R' A B' ->
-    R = R'.
+Add Parametric Morphism i : (per_univ_elem i)
+    with signature (@relation_equivalence domain) ==> eq ==> eq ==> iff as per_univ_elem_morphism_iff.
+Proof with mautosolve.
+  simpl.
+  intros R R' HRR'.
+  split; intros Horig; [gen R' | gen R];
+    induction Horig using per_univ_elem_ind; per_univ_elem_econstructor; eauto;
+    try (etransitivity; [symmetry + idtac|]; eassumption);
+    intros;
+    destruct_rel_mod_eval;
+    econstructor...
+Qed.
+
+Add Parametric Morphism i : (per_univ_elem i)
+    with signature (@relation_equivalence domain) ==> (@relation_equivalence domain) as per_univ_elem_morphism_relation_equivalence.
 Proof with mautosolve.
+  intros ** a b.
+  simpl.
+  rewrite H.
+  reflexivity.
+Qed.
+
+Add Parametric Morphism i A p A' p' : (rel_typ i A p A' p')
+    with signature (@relation_equivalence domain) ==> iff as rel_typ_morphism.
+Proof.
+  intros * HRR'.
+  split; intros []; econstructor; try eassumption;
+    [setoid_rewrite <- HRR' | setoid_rewrite HRR']; eassumption.
+Qed.
+
+Ltac rewrite_relation_equivalence_left :=
+  repeat match goal with
+    | H : ?R1 <~> ?R2 |- _ =>
+        try setoid_rewrite H;
+        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite H in H');
+        let T := type of H in
+        fold (id T) in H
+    end; unfold id in *.
+
+Ltac rewrite_relation_equivalence_right :=
+  repeat match goal with
+    | H : ?R1 <~> ?R2 |- _ =>
+        try setoid_rewrite H;
+        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite <- H in H');
+        let T := type of H in
+        fold (id T) in H
+    end; unfold id in *.
+
+Ltac clear_relation_equivalence :=
+  repeat match goal with
+    | H : ?R1 <~> ?R2 |- _ =>
+        (unify R1 R2; clear H) + (is_var R1; clear R1 H) + (is_var R2; clear R2 H)
+    end.
+
+Ltac apply_relation_equivalence := rewrite_relation_equivalence_right; clear_relation_equivalence; rewrite_relation_equivalence_left; clear_relation_equivalence.
+
+Lemma per_univ_elem_right_irrel : forall i i' R a b R' b',
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ DF a ≈ b' ∈ per_univ_elem i' ↘ R' }} ->
+    (R <~> R').
+Proof with (destruct_rel_mod_eval; destruct_rel_mod_app; functional_eval_rewrite_clear; econstructor; intuition).
+  simpl.
   intros * Horig.
-  remember A as A' in |- *.
-  gen A' B' R'.
+  remember a as a' in |- *.
+  gen a' b' R'.
   induction Horig using per_univ_elem_ind; intros * Heq Hright;
     subst; invert_per_univ_elem Hright; unfold per_univ;
-    trivial.
+    intros;
+    apply_relation_equivalence;
+    try reflexivity.
   specialize (IHHorig _ _ _ eq_refl equiv_a_a').
-  subst.
-  extensionality f.
-  extensionality f'.
-  (on_all_hyp: fun H => rewrite H).
-  extensionality c.
-  extensionality c'.
-  extensionality equiv_c_c'.
-  destruct_rel_mod_eval.
-  functional_eval_rewrite_clear.
-  f_equal...
+  split; intros.
+  - rename equiv_c_c' into equiv0_c_c'.
+    assert (equiv_c_c' : in_rel c c') by firstorder...
+  - assert (equiv0_c_c' : in_rel0 c c') by firstorder...
 Qed.
 
 #[local]
-Ltac per_univ_elem_right_irrel_rewrite1 :=
+Ltac per_univ_elem_right_irrel_assert1 :=
   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 first [solve [eauto using per_univ_elem_right_irrel] | fail 3]
+  | H1 : {{ DF ~?a ≈ ~?b ∈ per_univ_elem ?i ↘ ?R1 }},
+      H2 : {{ DF ~?a ≈ ~?b' ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+      assert_fails (unify R1 R2);
+      match goal with
+      | H : R1 <~> R2 |- _ => fail 1
+      | H : R2 <~> R1 |- _ => fail 1
+      | _ => assert (R1 <~> R2) by (eapply per_univ_elem_right_irrel; [apply H1 | apply H2])
+      end
   end.
 #[local]
-Ltac per_univ_elem_right_irrel_rewrite := repeat per_univ_elem_right_irrel_rewrite1.  
-
-Lemma per_univ_elem_sym : forall i R A B,
-    per_univ_elem i R A B ->
-    per_univ_elem i R B A /\
-      (forall a b,
-          {{ Dom a ≈ b ∈ R }} ->
-          {{ Dom b ≈ a ∈ R }}).
-Proof with (try econstructor; mautosolve).
-  induction 1 using per_univ_elem_ind; subst.
+Ltac per_univ_elem_right_irrel_assert := repeat per_univ_elem_right_irrel_assert1.
+
+Lemma per_univ_elem_sym : forall i R a b,
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ DF b ≈ a ∈ per_univ_elem i ↘ R }} /\
+      (forall m m',
+          {{ Dom m ≈ m' ∈ R }} ->
+          {{ Dom m' ≈ m ∈ R }}).
+Proof with mautosolve.
+  simpl.
+  induction 1 using per_univ_elem_ind; subst;
+    (* why does rewrite on <~> works only with this? *)
+    pose proof (@relation_equivalence_pointwise domain).
   - split.
-    + apply per_univ_elem_core_univ'...
-    + intros * [? []%H1]...
-  - split...
+    + apply per_univ_elem_core_univ'; firstorder.
+    + intros.
+      rewrite H1 in *.
+      destruct_by_head per_univ.
+      eexists.
+      eapply proj1...
+  - split; [per_univ_elem_econstructor | intros; apply_relation_equivalence]...
   - destruct_conjs.
-    (on_all_hyp: fun H => setoid_rewrite H).
     split.
     + per_univ_elem_econstructor; eauto.
       intros.
@@ -203,76 +296,95 @@ Proof with (try econstructor; mautosolve).
       assert (in_rel c c) by (etransitivity; eassumption).
       destruct_rel_mod_eval.
       functional_eval_rewrite_clear.
-      per_univ_elem_right_irrel_rewrite...
-    + enough (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')) by eauto.
+      econstructor; mauto.
+      per_univ_elem_right_irrel_assert.
+      apply_relation_equivalence.
+      eassumption.
+    + apply_relation_equivalence.
       intros.
       assert (in_rel c' c) by eauto.
       assert (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...
-  - split...
+      econstructor; mauto.
+      per_univ_elem_right_irrel_assert.
+      intuition.
+  - split; [econstructor | intros; apply_relation_equivalence]...
 Qed.
 
-Corollary per_univ_sym : forall i R A B,
-    per_univ_elem i R A B ->
-    per_univ_elem i R B A.
+Corollary per_univ_sym : forall i R a b,
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ DF b ≈ a ∈ per_univ_elem i ↘ R }}.
 Proof.
   intros * ?%per_univ_elem_sym.
   firstorder.
 Qed.
 
-Corollary per_elem_sym : forall i R A B a b,
-    per_univ_elem i R A B ->
-    R a b ->
-    R b a.
+Corollary per_elem_sym : forall i R a b m m',
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ Dom m ≈ m' ∈ R }} ->
+    {{ Dom m' ≈ m ∈ R }}.
 Proof.
   intros * ?%per_univ_elem_sym.
   firstorder.
 Qed.
 
-Corollary per_univ_elem_left_irrel : forall i i' R A B R' A',
-    per_univ_elem i R A B ->
-    per_univ_elem i' R' A' B ->
-    R = R'.
+Corollary per_univ_elem_left_irrel : forall i i' R a b R' a',
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ DF a' ≈ b ∈ per_univ_elem i' ↘ R' }} ->
+    (R <~> R').
 Proof.
   intros * ?%per_univ_sym ?%per_univ_sym.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Corollary per_univ_elem_cross_irrel : forall i i' R A B R' B',
-    per_univ_elem i R A B ->
-    per_univ_elem i' R' B' A ->
-    R = R'.
+Corollary per_univ_elem_cross_irrel : forall i i' R a b R' b',
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ DF b' ≈ a ∈ per_univ_elem i' ↘ R' }} ->
+    (R <~> R').
 Proof.
   intros * ? ?%per_univ_sym.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Ltac do_per_univ_elem_irrel_rewrite1 :=
-  let tactic_error o1 o2 := fail 3 "per_univ_elem_irrel equality between" o1 "and" o2 "cannot be solved by eauto" in
+Ltac do_per_univ_elem_irrel_assert1 :=
+  let tactic_error o1 o2 := fail 2 "per_univ_elem_irrel biconditional between" o1 "and" o2 "cannot be solved" in
   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 first [solve [eauto using per_univ_elem_right_irrel] | tactic_error R2 R1]
-    | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
-        H2 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by first [solve [eauto using per_univ_elem_left_irrel] | tactic_error R2 R1]
-    | 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 first [solve [symmetry; eauto using per_univ_elem_cross_irrel] | tactic_error R2 R1]
-    end.
+  | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
+      H2 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+      assert_fails (unify R1 R2);
+      match goal with
+      | H : R1 <~> R2 |- _ => fail 1
+      | H : R2 <~> R1 |- _ => fail 1
+      | _ => assert (R1 <~> R2) by (eapply per_univ_elem_right_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
+      end
+  | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
+      H2 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i' ↘ ?R2 }} |- _ =>
+      assert_fails (unify R1 R2);
+      match goal with
+      | H : R1 <~> R2 |- _ => fail 1
+      | H : R2 <~> R1 |- _ => fail 1
+      | _ => assert (R1 <~> R2) by (eapply per_univ_elem_left_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
+      end
+  | 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 *)
+      assert_fails (unify R1 R2);
+      match goal with
+      | H : R1 <~> R2 |- _ => fail 1
+      | H : R2 <~> R1 |- _ => fail 1
+      | _ => assert (R1 <~> R2) by (eapply per_univ_elem_cross_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
+      end
+  end.
 
-Ltac do_per_univ_elem_irrel_rewrite :=
-  repeat do_per_univ_elem_irrel_rewrite1.
+Ltac do_per_univ_elem_irrel_assert :=
+  repeat do_per_univ_elem_irrel_assert1.
 
-Ltac per_univ_elem_irrel_rewrite :=
+Ltac handle_per_univ_elem_irrel :=
   functional_eval_rewrite_clear;
-  do_per_univ_elem_irrel_rewrite;
+  do_per_univ_elem_irrel_assert;
+  apply_relation_equivalence;
   clear_dups.
 
 Lemma per_univ_elem_trans : forall i R A1 A2,
@@ -284,32 +396,45 @@ Lemma per_univ_elem_trans : forall i R A1 A2,
           R a1 a2 ->
           R a2 a3 ->
           R a1 a3).
-Proof with ((econstructor + per_univ_elem_econstructor); mautosolve).
+Proof with (per_univ_elem_econstructor; mautosolve).
+  pose proof (@relation_equivalence_pointwise domain).
   induction 1 using per_univ_elem_ind;
     [> split;
      [ intros * HT2; invert_per_univ_elem HT2; clear HT2
-     | intros * HTR1 HTR2 ] ..]; mauto.
-  - destruct HTR1, HTR2.
-    per_univ_elem_irrel_rewrite.
-    specialize (H1 _ _ _ H2) as [].
-    specialize (H0 _ _ H3)...
-  - idtac...
-  - per_univ_elem_irrel_rewrite.
-    rename in_rel0 into in_rel.
-    destruct IHper_univ_elem as [].
+     | intros * HTR1 HTR2; apply_relation_equivalence ] ..]; mauto.
+  - (* univ case *)
+    subst.
+    destruct HTR1, HTR2.
+    functional_eval_rewrite_clear.
+    handle_per_univ_elem_irrel.
+    specialize (H3 _ _ _ H1) as [].
+    eexists.
+    intuition.
+  - (* nat case *)
+    idtac...
+  - (* pi case *)
+    destruct_conjs.
     per_univ_elem_econstructor; eauto.
+    + handle_per_univ_elem_irrel.
+      intuition.
+    + intros.
+      handle_per_univ_elem_irrel.
+      assert (in_rel c c') by firstorder.
+      assert (in_rel c c) by intuition.
+      assert (in_rel0 c c) by intuition.
+      destruct_rel_mod_eval.
+      functional_eval_rewrite_clear.
+      handle_per_univ_elem_irrel...
+  - (* fun case *)
     intros.
-    assert (in_rel c c) by (etransitivity; [ | symmetry]; eassumption).
-    destruct_rel_mod_eval.
-    per_univ_elem_irrel_rewrite...
-  - destruct IHper_univ_elem as [].
-    rewrite H2 in *.
-    intros.
-    assert (in_rel c' c') by (etransitivity; [symmetry | ]; eassumption).
+    assert (in_rel c c) by intuition.
     destruct_rel_mod_eval.
     destruct_rel_mod_app.
-    per_univ_elem_irrel_rewrite...
-  - idtac...
+    handle_per_univ_elem_irrel.
+    econstructor; eauto.
+    intuition.
+  - (* neut case *)
+    idtac...
 Qed.
 
 Corollary per_univ_trans : forall i j R A1 A2 A3,
@@ -331,22 +456,20 @@ Proof.
   firstorder.
 Qed.
 
-
 #[export]
-  Instance per_elem_PER {i R A B} `(H : per_univ_elem i R A B) : PER R.
+Instance per_univ_PER {i R} : PER (per_univ_elem i R).
 Proof.
   split.
-  - auto using (per_elem_sym _ _ _ _ _ _ H).
-  - eauto using (per_elem_trans _ _ _ _ _ _ _ H).
+  - auto using per_univ_sym.
+  - eauto using per_univ_trans.
 Qed.
 
-
 #[export]
-  Instance per_univ_PER {i R} : PER (per_univ_elem i R).
+Instance per_elem_PER {i R A B} `(H : per_univ_elem i R A B) : PER R.
 Proof.
   split.
-  - auto using per_univ_sym.
-  - eauto using per_univ_trans.
+  - eauto using (per_elem_sym _ _ _ _ _ _ H).
+  - eauto using (per_elem_trans _ _ _ _ _ _ _ H).
 Qed.
 
 (* This lemma gets rid of the unnecessary PER premise. *)
@@ -357,7 +480,7 @@ Lemma per_univ_elem_core_pi' :
     (equiv_a_a' : {{ DF A ≈ A' ∈ per_univ_elem i ↘ in_rel}}),
     (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
         rel_mod_eval (per_univ_elem i) 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') ->
+    (elem_rel <~> fun f f' => forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}), rel_mod_app f c f' c' (out_rel equiv_c_c')) ->
     {{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }}.
 Proof.
   intros.
@@ -365,7 +488,6 @@ Proof.
   typeclasses eauto.
 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 }}.
@@ -373,7 +495,7 @@ Proof with solve [eauto].
   simpl.
   induction 1 using per_univ_elem_ind; subst.
   - eapply per_univ_elem_core_univ'...
-  - per_univ_elem_econstructor.
+  - per_univ_elem_econstructor...
   - per_univ_elem_econstructor; mauto.
     intros.
     destruct_rel_mod_eval.
@@ -381,24 +503,39 @@ Proof with solve [eauto].
   - per_univ_elem_econstructor...
 Qed.
 
+Add Parametric Morphism : per_ctx_env
+    with signature (@relation_equivalence env) ==> eq ==> eq ==> iff as per_ctx_env_morphism_iff.
+Proof with mautosolve.
+  intros R R' HRR'.
+  split; intro Horig; [gen R' | gen R];
+    induction Horig; econstructor;
+    apply_relation_equivalence; try reflexivity...
+Qed.
+
+Add Parametric Morphism : per_ctx_env
+    with signature (@relation_equivalence env) ==> (@relation_equivalence ctx) as per_ctx_env_morphism_relation_equivalence.
+Proof with mautosolve.
+  intros * HRR' Γ Γ'.
+  simpl.
+  rewrite HRR'.
+  reflexivity.
+Qed.
+
 Lemma per_ctx_env_right_irrel : forall Γ Δ Δ' R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Γ ≈ Δ' ∈ per_ctx_env ↘ R' }} ->
-    R = R'.
-Proof.
+    R <~> R'.
+Proof with (destruct_rel_typ; handle_per_univ_elem_irrel; eexists; intuition).
   intros * Horig; gen Δ' R'.
   induction Horig; intros * Hright;
-    inversion Hright; subst; try congruence.
+    inversion Hright; subst;
+    apply_relation_equivalence;
+    try reflexivity.
   specialize (IHHorig _ _ equiv_Γ_Γ'0).
-  subst.
-  enough (head_rel = head_rel0) by now subst.
-  extensionality p.
-  extensionality p'.
-  extensionality equiv_p_p'.
-  simpl in *.
-  destruct_rel_mod_eval.
-  per_univ_elem_irrel_rewrite.
-  congruence.
+  intros p p'.
+  split; intros [].
+  - assert (equiv0_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel0 }}) by intuition...
+  - assert (equiv_p_drop_p'_drop : {{ Dom p ↯ ≈ p' ↯ ∈ tail_rel }}) by intuition...
 Qed.
 
 Lemma per_ctx_env_sym : forall Γ Δ R,
@@ -407,25 +544,23 @@ Lemma per_ctx_env_sym : forall Γ Δ R,
       (forall o p,
           {{ Dom o ≈ p ∈ R }} ->
           {{ Dom p ≈ o ∈ R }}).
-Proof with solve [eauto using per_univ_sym].
+Proof with solve [intuition].
   simpl.
-  induction 1; split; try solve [econstructor; eauto]; simpl in *; destruct_conjs.
-  - econstructor; eauto.
-    intros.
-    assert (tail_rel p' p) by eauto.
-    assert (tail_rel p p) by (etransitivity; eauto).
+  induction 1; split; simpl in *; destruct_conjs; try econstructor; intuition;
+    pose proof (@relation_equivalence_pointwise env).
+  - assert (tail_rel p' p) by eauto.
+    assert (tail_rel p p) by (etransitivity; eassumption).
     destruct_rel_mod_eval.
-    per_univ_elem_irrel_rewrite.
-    econstructor...
-  - subst.
-    intros.
+    handle_per_univ_elem_irrel.
+    econstructor; eauto.
+    symmetry...
+  - apply_relation_equivalence.
     destruct_conjs.
     assert (tail_rel d{{{ p ↯ }}} d{{{ o ↯ }}}) by eauto.
-    assert (tail_rel d{{{ p ↯ }}} d{{{ p ↯ }}}) by (etransitivity; eauto).
+    assert (tail_rel d{{{ p ↯ }}} d{{{ p ↯ }}}) by (etransitivity; eassumption).
     destruct_rel_mod_eval.
     eexists.
-    per_univ_elem_irrel_rewrite.
-    eapply per_elem_sym...
+    handle_per_univ_elem_irrel; symmetry; intuition.
 Qed.
 
 Corollary per_ctx_sym : forall Γ Δ R,
@@ -448,7 +583,7 @@ Qed.
 Corollary per_ctx_env_left_irrel : forall Γ Γ' Δ R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Γ' ≈ Δ ∈ per_ctx_env ↘ R' }} ->
-    R = R'.
+    R <~> R'.
 Proof.
   intros * ?%per_ctx_sym ?%per_ctx_sym.
   eauto using per_ctx_env_right_irrel.
@@ -457,33 +592,49 @@ Qed.
 Corollary per_ctx_env_cross_irrel : forall Γ Δ Δ' R R',
     {{ DF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
     {{ DF Δ' ≈ Γ ∈ per_ctx_env ↘ R' }} ->
-    R = R'.
+    R <~> R'.
 Proof.
   intros * ? ?%per_ctx_sym.
   eauto using per_ctx_env_right_irrel.
 Qed.
 
-Ltac do_per_ctx_env_irrel_rewrite1 :=
+Ltac do_per_ctx_env_irrel_assert1 :=
   let tactic_error o1 o2 := fail 3 "per_ctx_env_irrel equality between" o1 "and" o2 "cannot be solved by mauto" in
   match goal with
     | H1 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R1 }},
         H2 : {{ DF ~?Γ ≈ ~_ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by first [solve [eauto using per_ctx_env_right_irrel] | tactic_error R2 R1]
+        assert_fails (unify R1 R2);
+        match goal with
+        | H : R1 <~> R2 |- _ => fail 1
+        | H : R2 <~> R1 |- _ => fail 1
+        | _ => assert (R1 <~> R2) by (eapply per_ctx_env_right_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
+        end
     | H1 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?Δ ∈ per_ctx_env ↘ ?R2 }} |- _ =>
-        clean replace R2 with R1 by first [solve [eauto using per_ctx_env_left_irrel] | tactic_error R2 R1]
+        assert_fails (unify R1 R2);
+        match goal with
+        | H : R1 <~> R2 |- _ => fail 1
+        | H : R2 <~> R1 |- _ => fail 1
+        | _ => assert (R1 <~> R2) by (eapply per_ctx_env_left_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
+        end
     | 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 first [solve [symmetry; eauto using per_ctx_env_cross_irrel] | tactic_error R2 R1]
+        assert_fails (unify R1 R2);
+        match goal with
+        | H : R1 <~> R2 |- _ => fail 1
+        | H : R2 <~> R1 |- _ => fail 1
+        | _ => assert (R1 <~> R2) by (eapply per_ctx_env_cross_irrel; [apply H1 | apply H2]) || tactic_error R1 R2
+        end
     end.
 
-Ltac do_per_ctx_env_irrel_rewrite :=
-  repeat do_per_ctx_env_irrel_rewrite1.
+Ltac do_per_ctx_env_irrel_assert :=
+  repeat do_per_ctx_env_irrel_assert1.
 
-Ltac per_ctx_env_irrel_rewrite :=
+Ltac handle_per_ctx_env_irrel :=
   functional_eval_rewrite_clear;
-  do_per_ctx_env_irrel_rewrite;
+  do_per_ctx_env_irrel_assert;
+  apply_relation_equivalence;
   clear_dups.
 
 Lemma per_ctx_env_trans : forall Γ1 Γ2 R,
@@ -500,21 +651,27 @@ Proof with solve [eauto using per_univ_trans].
   induction 1; subst;
     [> split;
      [ inversion 1; subst; eauto
-     | intros; destruct_conjs; unfold per_total; eauto] ..];
-    per_ctx_env_irrel_rewrite.
-  - rename tail_rel0 into tail_rel.
-    econstructor; eauto.
-    + eapply IHper_ctx_env...
+     | intros; destruct_conjs; eauto] ..];
+    pose proof (@relation_equivalence_pointwise env);
+    handle_per_ctx_env_irrel;
+    try solve [intuition].
+  - econstructor; only 4: reflexivity; eauto.
+    + apply_relation_equivalence. intuition.
     + intros.
-      assert (tail_rel p p) by (etransitivity; [| symmetry]; eauto).
-      (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
-      per_univ_elem_irrel_rewrite.
-      econstructor...
-  - assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by mauto.
+      assert (tail_rel p p) by intuition.
+      assert (tail_rel0 p p') by intuition.
+      destruct_rel_typ.
+      handle_per_univ_elem_irrel.
+      econstructor; intuition.
+      (* This one cannot be replaced with `etransitivity` as we need different `i`s. *)
+      eapply per_univ_trans; [| eassumption]; eassumption.
+  - destruct_conjs.
+    assert (tail_rel d{{{ p1 ↯ }}} d{{{ p3 ↯ }}}) by eauto.
+    destruct_rel_typ.
+    handle_per_univ_elem_irrel.
     eexists.
-    (on_all_hyp: fun H => destruct_rel_by_assumption tail_rel H).
-    per_univ_elem_irrel_rewrite.
-    eapply per_elem_trans...
+    apply_relation_equivalence.
+    etransitivity; intuition.
 Qed.
 
 Corollary per_ctx_trans : forall Γ1 Γ2 Γ3 R,
@@ -536,18 +693,16 @@ Proof.
   firstorder.
 Qed.
 
-
 #[export]
-  Instance per_ctx_PER {R} : PER (per_ctx_env R).
+Instance per_ctx_PER {R} : PER (per_ctx_env R).
 Proof.
   split.
   - auto using per_ctx_sym.
   - eauto using per_ctx_trans.
 Qed.
 
-
 #[export]
-  Instance per_env_PER {R Γ Δ} (H : per_ctx_env R Γ Δ) : PER R.
+Instance per_env_PER {R Γ Δ} (H : per_ctx_env R Γ Δ) : PER R.
 Proof.
   split.
   - auto using (per_env_sym _ _ _ _ _ H).
diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v
index 54b0936a..69c0210d 100644
--- a/theories/Core/Semantic/Realizability.v
+++ b/theories/Core/Semantic/Realizability.v
@@ -1,4 +1,4 @@
-From Coq Require Import Lia PeanoNat Relation_Definitions.
+From Coq Require Import Lia Morphisms_Relations PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
 From Mcltt Require Import Base Evaluation LibTactics Readback.
 From Mcltt Require Export PER.
@@ -22,49 +22,49 @@ Lemma realize_per_univ_elem_gen : forall {i a a' R},
     /\ (forall {c c'}, {{ Dom c ≈ c' ∈ per_bot }} -> {{ Dom ⇑ a c ≈ ⇑ a' c' ∈ R }})
     /\ (forall {b b'}, {{ Dom b ≈ b' ∈ R }} -> {{ Dom ⇓ a b ≈ ⇓ a' b' ∈ per_top }}).
 Proof with (solve [try (try (eexists; split); econstructor); mauto]).
-  intros * H. simpl in H.
-  induction H using per_univ_elem_ind; repeat split; intros.
-  - subst...
-  - eexists.
+  pose proof (@relation_equivalence_pointwise domain).
+  intros * Hunivelem. simpl in Hunivelem.
+  induction Hunivelem using per_univ_elem_ind; repeat split; intros;
+    apply_relation_equivalence; mauto.
+  - subst; repeat econstructor.
+  - subst.
+    eexists.
     per_univ_elem_econstructor...
-  - destruct_by_head per_univ.
-    specialize (H1 _ _ _ H2).
+  - subst.
+    destruct_by_head per_univ.
+    specialize (H3 _ _ _ H1).
     destruct_conjs.
     intro s.
-    specialize (H1 s) as [? []]...
+    specialize (H2 s) as [? []]...
   - idtac...
-  - idtac...
-  - eauto using per_nat_then_per_top.
-  - destruct IHper_univ_elem as [? []].
+  - apply_relation_equivalence...
+  - destruct IHHunivelem as [? []].
     intro s.
     assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
     destruct_rel_mod_eval.
     specialize (H10 (S s)) as [? []].
     specialize (H3 s) as [? []]...
-  - (on_all_hyp: fun H => rewrite H in *; clear H).
-    intros c0 c0' equiv_c0_c0'.
+  - intros c0 c0' equiv_c0_c0'.
     destruct_conjs.
     destruct_rel_mod_eval.
     econstructor; try solve [econstructor; eauto].
     enough ({{ Dom c ⇓ A c0 ≈ c' ⇓ A' c0' ∈ per_bot }}) by eauto.
     intro s.
-    specialize (H3 s) as [? []].
-    specialize (H5 _ _ equiv_c0_c0' s) as [? []]...
-  - (on_all_hyp: fun H => rewrite H in *; clear H).
-    destruct_conjs.
+    specialize (H4 s) as [? []].
+    specialize (H6 _ _ equiv_c0_c0' s) as [? []]...
+  - destruct_conjs.
     intro s.
     assert {{ Dom ⇑! A s ≈ ⇑! A' s ∈ in_rel }} by eauto using var_per_bot.
     destruct_rel_mod_eval.
     destruct_rel_mod_app.
     assert {{ Dom ⇓ a fa ≈ ⇓ a' f'a' ∈ per_top }} by eauto.
-    specialize (H2 s) as [? []].
-    specialize (H16 (S s)) as [? []]...
+    specialize (H3 s) as [? []].
+    specialize (H17 (S s)) as [? []]...
   - intro s.
     (on_all_hyp: fun H => destruct (H s) as [? []])...
   - idtac...
   - intro s.
-    (on_all_hyp: fun H => specialize (H s) as [? []]).
-    (on_all_hyp: fun H => inversion_clear H; let n := numgoals in guard n <= 1).
+    inversion_clear_by_head per_ne.
     (on_all_hyp: fun H => specialize (H s) as [? []])...
 Qed.
 
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 38299cf1..5f46d32d 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -77,7 +77,7 @@ Ltac find_dup_hyp tac non :=
     not_let_bind H';
     lazymatch type of X with
     | Prop => tac H H' X
-    | _ => idtac
+    | _ => fail
     end
   | _ => non
   end.
@@ -159,3 +159,6 @@ Ltac mautosolve := unshelve solve [mauto]; solve [constructor].
 
 #[export]
   Hint Extern 1 => eassumption : typeclass_instances.
+
+(* intuition tactic default setting *)
+Ltac Tauto.intuition_solver ::= auto with mcltt core solve_subterm.
diff --git a/theories/_CoqProject b/theories/_CoqProject
index c3e016f1..21323536 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -4,7 +4,10 @@
 
 ./Core/Axioms.v
 ./Core/Base.v
+./Core/Completeness/LogicalRelation/Definitions.v
+./Core/Completeness/LogicalRelation/Lemmas.v
 ./Core/Completeness/LogicalRelation.v
+./Core/Completeness/FunctionCases.v
 ./Core/Completeness/TermStructureCases.v
 ./Core/Completeness/UniverseCases.v
 ./Core/Completeness/VariableCases.v
@@ -13,6 +16,7 @@
 ./Core/Semantic/Evaluation/Definitions.v
 ./Core/Semantic/Evaluation/Lemmas.v
 ./Core/Semantic/PER.v
+./Core/Semantic/PER/CoreTactics.v
 ./Core/Semantic/PER/Definitions.v
 ./Core/Semantic/PER/Lemmas.v
 ./Core/Semantic/Readback.v