diff --git a/theories/Core/Semantic/EvaluateLemmas.v b/theories/Core/Semantic/EvaluateLemmas.v
index 5e51929a..fe19d14f 100644
--- a/theories/Core/Semantic/EvaluateLemmas.v
+++ b/theories/Core/Semantic/EvaluateLemmas.v
@@ -64,14 +64,15 @@ End functional_eval.
 #[export]
 Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_sub : mcltt.
 
-Ltac functional_eval_rewrite_clear := 
-  repeat match goal with
-    | H1 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m2 }} |- _ =>
-        assert (m1 = m2) by mauto; subst; clear H2
-    | H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
-        assert (r1 = r2) by mauto; subst; clear H2
-    | H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r2 }} |- _ =>
-        assert (r1 = r2) by mauto; subst; clear H2
-    | H1 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p2 }} |- _ =>
-        assert (p1 = p2) by mauto; subst; clear H2
-    end.
+Ltac functional_eval_rewrite_clear1 :=
+  match goal with
+  | H1 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m1 }}, H2 : {{ ⟦ ~?M ⟧ ~?p ↘ ~?m2 }} |- _ =>
+      clean replace m2 with m1 by mauto; clear H2
+  | H1 : {{ $| ~?m & ~?n |↘ ~?r1 }}, H2 : {{ $| ~?m & ~?n |↘ ~?r2 }} |- _ =>
+      clean replace r2 with r1 by mauto; clear H2
+  | H1 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r1 }}, H2 : {{ rec ~?m ⟦return ~?A | zero -> ~?MZ | succ -> ~?MS end⟧ ~?p ↘ ~?r2 }} |- _ =>
+      clean replace r2 with r1 by mauto; clear H2
+  | H1 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p1 }}, H2 : {{ ⟦ ~?σ ⟧s ~?p ↘ ~?p2 }} |- _ =>
+      clean replace p2 with p1 by mauto; clear H2
+  end.
+Ltac functional_eval_rewrite_clear := repeat functional_eval_rewrite_clear1.
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index 30acfdca..33eb71d3 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -169,43 +169,6 @@ Section Per_univ_elem_ind_def.
 
 End Per_univ_elem_ind_def.
 
-Lemma rel_mod_eval_ex_pull :
-  forall (A : Type) (P : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R,
-    rel_mod_eval (fun a b R => exists x : A, P a b R x) T p T' p' R <->
-      exists x : A, rel_mod_eval (fun a b R => P a b R x) T p T' p' R.
-Proof.
-  split; intros.
-  - destruct H.
-    destruct H1 as [? ?].
-    eexists; econstructor; eauto.
-  - do 2 destruct H; econstructor; eauto.
-Qed.
-
-Lemma rel_mod_eval_simp_ex :
-  forall (A : Type) (P : domain -> domain -> relation domain -> Prop) (Q : domain -> domain -> relation domain -> A -> Prop) {T p T' p'} R,
-    rel_mod_eval (fun a b R => P a b R /\ exists x : A, Q a b R x) T p T' p' R <->
-      exists x : A, rel_mod_eval (fun a b R => P a b R /\ Q a b R x) T p T' p' R.
-Proof.
-  split; intros.
-  - destruct H.
-    destruct H1 as [? [? ?]].
-    eexists; econstructor; eauto.
-  - do 2 destruct H; econstructor; eauto.
-    firstorder.
-Qed.
-
-Lemma rel_mod_eval_simp_and :
-  forall (P : domain -> domain -> relation domain -> Prop) (Q : relation domain -> Prop) {T p T' p'} R,
-    rel_mod_eval (fun a b R => P a b R /\ Q R) T p T' p' R <->
-      rel_mod_eval P T p T' p' R /\ Q R.
-Proof.
-  split; intros.
-  - destruct H.
-    destruct H1 as [? ?].
-    split; try econstructor; eauto.
-  - do 2 destruct H; econstructor; eauto.
-Qed.
-
 Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
 
 Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index c832b5b5..c9d177ec 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -2,6 +2,43 @@ From Coq Require Import Lia PeanoNat Relations.Relation_Definitions RelationClas
 From Equations Require Import Equations.
 From Mcltt Require Import Axioms Base Domain Evaluate EvaluateLemmas LibTactics PER Readback ReadbackLemmas Syntax System.
 
+(* 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 }}.
@@ -84,6 +121,30 @@ Ltac per_univ_elem_econstructor :=
   econstructor;
   try rewrite <- per_univ_elem_equation_1 in *.
 
+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.
+
 Lemma per_univ_elem_right_irrel_gen : forall i A B R,
     per_univ_elem i A B R ->
     forall A' B' R',
@@ -103,10 +164,9 @@ Proof.
   extensionality c.
   extensionality c'.
   extensionality equiv_c_c'.
-  specialize (H1 _ _ equiv_c_c') as [? ? ? ? []].
-  specialize (H9 _ _ equiv_c_c') as [? ? ? ? ?].
+  destruct_rel_mod_eval.
   functional_eval_rewrite_clear.
-  specialize (H5 _ _ _ eq_refl H9).
+  specialize (H12 _ _ _ eq_refl H5).
   congruence.
 Qed.
 
@@ -118,21 +178,12 @@ Proof.
   intros. eauto using per_univ_elem_right_irrel_gen.
 Qed.
 
-Ltac per_univ_elem_right_irrel_rewrite :=
-  repeat match goal with
-    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
-        mark H2
-    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B' ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-        assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; mark H2
-    end; unmark_all.
-
-Ltac functional_per_univ_elem_rewrite_clear :=
-  repeat match goal with
-    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }} |- _ =>
-        clear H2
-    | H1 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }}, H2 : {{ DF ~?A ≈ ~?B ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-        assert (R2 = R1) by (eapply per_univ_elem_right_irrel; eassumption); subst; clear H2
-    end.
+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 ->
@@ -141,7 +192,7 @@ Proof.
   intros. induction H using per_univ_elem_ind; subst.
   - split.
     + apply per_univ_elem_core_univ'; trivial.
-    + intros. split; intros HD; destruct HD.
+    + intros. split; intros [].
       * specialize (H1 _ _ _ H0).
         firstorder.
       * specialize (H1 _ _ _ H0).
@@ -156,28 +207,24 @@ Proof.
       intros.
       assert (equiv_c'_c : in_rel c' c) by firstorder.
       assert (equiv_c_c : in_rel c c) by (etransitivity; eassumption).
-      destruct (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
-      destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
-      destruct (H1 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
+      destruct_rel_mod_eval.
       econstructor; eauto.
       functional_eval_rewrite_clear.
       per_univ_elem_right_irrel_rewrite.
-      congruence.
+      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')). {
+                 (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 (H1 _ _ equiv_c_c') as [? ? ? ? [? [? ?]]].
-        destruct (H1 _ _ equiv_c'_c) as [? ? ? ? [? [? ?]]].
-        destruct (H1 _ _ equiv_c_c) as [? ? ? ? [? [? ?]]].
-        destruct (H5 _ _ equiv_c'_c) as [? ? ? ? ?].
+        destruct_rel_mod_eval.
+        destruct_rel_mod_app.
         functional_eval_rewrite_clear.
         per_univ_elem_right_irrel_rewrite.
         econstructor; eauto.
-        rewrite H17, H16.
         firstorder.
       }
       firstorder.
@@ -191,10 +238,7 @@ Lemma per_univ_elem_left_irrel : forall i A B R A' R',
     per_univ_elem i A' B R' ->
     R = R'.
 Proof.
-  intros.
-  apply per_univ_elem_sym in H.
-  apply per_univ_elem_sym in H0.
-  destruct_all.
+  intros * []%per_univ_elem_sym []%per_univ_elem_sym.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
@@ -203,9 +247,7 @@ Lemma per_univ_elem_cross_irrel : forall i A B R B' R',
     per_univ_elem i B' A R' ->
     R = R'.
 Proof.
-  intros.
-  apply per_univ_elem_sym in H0.
-  destruct_all.
+  intros * ? []%per_univ_elem_sym.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
@@ -213,19 +255,14 @@ 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 }} |- _ =>
-        tryif unify R1 R2 then fail else
-          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_right_irrel; eassumption); subst;
-                                 try rewrite <- H in *)
+        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 }} |- _ =>
-        tryif unify R1 R2 then fail else
-          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_left_irrel; eassumption); subst;
-                                 try rewrite <- H in *)
+        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 }} |- _ =>
-        tryif unify R1 R2 then fail else
-          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel; eassumption); subst;
-                                 try rewrite <- H in *)
+        (* 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 :=
@@ -245,32 +282,27 @@ Proof with solve [mauto].
   induction 1 using per_univ_elem_ind; intros * HT2;
     invert_per_univ_elem HT2; clear HT2.
   - split; mauto.
-    intros.
-    destruct H0, H2.
+    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).
-      specialize (H1 _ _ equiv_c_c) as [? ? ? ? [? ?]].
-      specialize (H9 _ _ equiv_c_c') as [].
+      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 (H1 _ _ equiv_c_c') as [? ? ? ? [? ?]].
-      specialize (H1 _ _ equiv_c'_c') as [? ? ? ? [? ?]].
-      specialize (H9 _ _ equiv_c'_c') as [].
-      specialize (H3 _ _ equiv_c_c') as [].
-      specialize (H4 _ _ equiv_c'_c') as [].
+      destruct_rel_mod_eval.
+      destruct_rel_mod_app.
       per_univ_elem_irrel_rewrite.
       firstorder (econstructor; eauto).
-
   - split; try per_univ_elem_econstructor...
 Qed.
diff --git a/theories/Core/Semantic/ReadbackLemmas.v b/theories/Core/Semantic/ReadbackLemmas.v
index a45e2bb0..58470fff 100644
--- a/theories/Core/Semantic/ReadbackLemmas.v
+++ b/theories/Core/Semantic/ReadbackLemmas.v
@@ -49,12 +49,13 @@ End functional_read.
 #[export]
 Hint Resolve functional_read_nf functional_read_ne functional_read_typ : mcltt.
 
-Ltac functional_read_rewrite_clear := 
-  repeat match goal with
-    | H1 : {{ Rnf ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rnf ~?m in ?s ↘ ~?M2 }} |- _ =>
-        idtac H1; assert (M1 = M2) by mauto; subst; clear H2
-    | H1 : {{ Rne ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rne ~?m in ?s ↘ ~?M2 }} |- _ =>
-        idtac H1; assert (M1 = M2) by mauto; subst; clear H2
-    | H1 : {{ Rtyp ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rtyp ~?m in ?s ↘ ~?M2 }} |- _ =>
-        idtac H1; assert (M1 = M2) by mauto; subst; clear H2
-    end.
+Ltac functional_read_rewrite_clear1 :=
+  match goal with
+  | H1 : {{ Rnf ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rnf ~?m in ?s ↘ ~?M2 }} |- _ =>
+      clean replace M2 with M1 by mauto; clear H2
+  | H1 : {{ Rne ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rne ~?m in ?s ↘ ~?M2 }} |- _ =>
+      clean replace M2 with M1 by mauto; clear H2
+  | H1 : {{ Rtyp ~?m in ?s ↘ ~?M1 }}, H2 : {{ Rtyp ~?m in ?s ↘ ~?M2 }} |- _ =>
+      clean replace M2 with M1 by mauto; clear H2
+  end.
+Ltac functional_read_rewrite_clear := repeat functional_read_rewrite_clear1.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 734ab1f6..2a38ce55 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -11,29 +11,41 @@ Tactic Notation "gen" ident(x) ident(y) ident(z) ident(w) := gen x y z; gen w.
 
 (** Marking-based Tactics *)
 
-Definition __mark__ A (a : A) : A := a.
-Arguments __mark__ {A} a : simpl never.
+Definition __mark__ (n : nat) A (a : A) : A := a.
+Arguments __mark__ n {A} a : simpl never.
 
 Ltac mark H :=
   let t := type of H in
-  fold (__mark__ t) in H.
+  fold (__mark__ 0 t) in H.
 Ltac unmark H := unfold __mark__ in H.
 
 Ltac mark_all :=
   repeat match goal with [H: ?P |- _] =>
-    try (match P with __mark__ _ => fail 2 end); mark H
+    try (match P with __mark__ _ _ => fail 2 end); mark H
   end.
 Ltac unmark_all := unfold __mark__ in *.
 
 Ltac on_all_marked_hyp tac :=
   match goal with
-  | [ H : __mark__ ?A |- _ ] => unmark H; tac H; on_all_marked_hyp tac; mark H
+  | [ H : __mark__ _ ?A |- _ ] => unmark H; tac H; on_all_marked_hyp tac; mark H
   | _ => idtac
   end.
 Tactic Notation "on_all_marked_hyp:" tactic4(tac) := on_all_marked_hyp tac.
 Tactic Notation "on_all_hyp:" tactic4(tac) :=
   mark_all; (on_all_marked_hyp: tac); unmark_all.
 
+Ltac mark_with H n :=
+  let t := type of H in
+  fold (__mark__ n t) in H.
+Ltac mark_all_with n :=
+  repeat match goal with [H: ?P |- _] =>
+    try (match P with __mark__ _ _ => fail 2 end); mark_with H n
+  end.
+Ltac unmark_all_with n :=
+  repeat match goal with [H: ?P |- _] =>
+    match P with __mark__ ?n' _ => tryif unify n n' then unmark H else fail 2 end
+  end.
+
 (** Simple helper *)
 
 Ltac destruct_logic :=
@@ -80,6 +92,17 @@ Ltac clear_dups :=
   repeat find_dup_hyp ltac:(fun H H' _ => clear H || clear H')
                              ltac:(idtac).
 
+Ltac clean_replace_by exp0 exp1 tac :=
+  tryif unify exp0 exp1
+  then fail
+  else
+    (let H := fresh "H" in
+     assert (exp0 = exp1) as H by ltac:(tac);
+     subst;
+     try rewrite <- H in *).
+
+Tactic Notation "clean" "replace" uconstr(exp0) "with" uconstr(exp1) "by" tactic3(tac) := clean_replace_by exp0 exp1 tac.
+
 (** McLTT automation *)
 
 Tactic Notation "mauto" :=