diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index 33eb71d3..40c43a05 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -9,11 +9,40 @@ Notation "'EF' a ≈ b ∈ R ↘ R'" := (R a b R' : Prop) (in custom judg at lev
 
 Generalizable All Variables.
 
-Inductive rel_mod_eval (R : domain -> domain -> relation domain -> Prop) A p A' p' R' : Prop := mk_rel_mod_eval : forall a a', {{ ⟦ A ⟧ p ↘ a }} -> {{ ⟦ A' ⟧ p' ↘ a' }} -> {{ DF a ≈ a' ∈ R ↘ R' }} -> rel_mod_eval R A p A' p' R'.
-Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
-
-Inductive rel_mod_app (R : relation domain) f a f' a' : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app R f a f' a'.
-Arguments mk_rel_mod_app {_ _ _ _ _}.
+(** Helper Bundles *)
+Section HelperBundles.
+  Inductive rel_mod_eval (R : domain -> domain -> relation domain -> Prop) A p A' p' R' : Prop := mk_rel_mod_eval : forall a a', {{ ⟦ A ⟧ p ↘ a }} -> {{ ⟦ A' ⟧ p' ↘ a' }} -> {{ DF a ≈ a' ∈ R ↘ R' }} -> rel_mod_eval R A p A' p' R'.
+  Arguments mk_rel_mod_eval {_ _ _ _ _ _}.
+
+  Inductive rel_mod_app (R : relation domain) f a f' a' : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app R f a f' a'.
+  Arguments mk_rel_mod_app {_ _ _ _ _}.
+
+  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.
+End HelperBundles.
+
+(** (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 }}).
 Arguments per_bot /.
@@ -40,6 +69,8 @@ Inductive per_ne : relation domain :=
      {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ per_ne }} }
 .
 
+(** Universe/Element PER Definition *)
+
 Section Per_univ_elem_core_def.
   Variable (i : nat) (per_univ_rec : forall {j}, j < i -> relation domain).
 
@@ -122,6 +153,8 @@ Proof.
 Qed.
 Global Hint Resolve per_univ_elem_core_univ' : mcltt.
 
+(** Universe/Element PER Induction Principle *)
+
 Section Per_univ_elem_ind_def.
   Hypothesis
     (motive : nat -> domain -> domain -> relation domain -> Prop).
@@ -169,6 +202,21 @@ Section Per_univ_elem_ind_def.
 
 End Per_univ_elem_ind_def.
 
+(** Universe/Element PER Helper Tactics *)
+
+Ltac invert_per_univ_elem H :=
+  simp per_univ_elem in H;
+  inversion H;
+  subst;
+  try rewrite <- per_univ_elem_equation_1 in *.
+
+Ltac per_univ_elem_econstructor :=
+  simp per_univ_elem;
+  econstructor;
+  try rewrite <- per_univ_elem_equation_1 in *.
+
+(** Context/Environment PER *)
+
 Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
 
 Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index c9d177ec..82737baa 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -110,41 +110,6 @@ Qed.
 #[export]
 Hint Resolve per_ne_trans : mcltt.
 
-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 *.
-
-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',