diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index 7c2011bf..95d58920 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -72,3 +72,31 @@ Proof with solve [mauto].
   Unshelve.
   all: assumption.
 Qed.
+
+Lemma per_univ_ind : forall i P,
+    (forall j j', j < i -> j = j' -> {{ Dom 𝕌@j ≈ 𝕌@j' ∈ P }}) ->
+    {{ Dom ℕ ≈ ℕ ∈ P }} ->
+    (forall a a' B p B' p'
+        (equiv_a_a' : {{ Dom a ≈ a' ∈ per_univ i }}),
+        {{ Dom a ≈ a' ∈ P }} ->
+        (forall c c',
+            {{ Dom c ≈ c' ∈ per_elem equiv_a_a' }} ->
+            rel_mod_eval (per_univ i) B d{{{ p ↦ c}}} B' d{{{ p' ↦ c'}}}) ->
+        {{ Dom Π a p B ≈ Π a' p' B' ∈ P }}) ->
+    (forall m m' a a', {{ Dom m ≈ m' ∈ per_bot }} -> {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ P }}) ->
+    forall d d', {{ Dom d ≈ d' ∈ per_univ i }} -> {{ Dom d ≈ d' ∈ P }}.
+Proof with solve [mauto].
+  intros * Huniv Hnat Hpi Hneut d d' [equiv_d_d'_template equiv_d_d'_check].
+  induction equiv_d_d'_check; only 1-2,4: solve [mauto].
+  unshelve epose (equiv_a_a'_real := _ : {{ Dom a ≈ a' ∈ per_univ i }}).
+  { econstructor... }
+  eapply Hpi with (equiv_a_a' := equiv_a_a'_real); subst equiv_a_a'_real; [solve [mauto]|].
+  intros * equiv_c_c'.
+  unfold per_elem, Per_univ_def.per_elem in equiv_c_c'.
+  destruct (rel_B_B' _ _ equiv_c_c').
+  econstructor; only 1-2: solve [mauto].
+  intros b b' eval_B eval_B'.
+  econstructor; apply H.
+  Unshelve.
+  3-5: eassumption.
+Qed.