diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v
index 506b4a5a..597b40c6 100644
--- a/theories/Core/Semantic/PER/CoreTactics.v
+++ b/theories/Core/Semantic/PER/CoreTactics.v
@@ -45,12 +45,12 @@ Ltac destruct_rel_typ :=
 (** Universe/Element PER Helper Tactics *)
 
 Ltac basic_invert_per_univ_elem H :=
-  simp per_univ_elem in H;
+  progress simp per_univ_elem in H;
   inversion H;
   subst;
   try rewrite <- per_univ_elem_equation_1 in *.
 
 Ltac basic_per_univ_elem_econstructor :=
-  simp per_univ_elem;
+  progress 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 a26e915d..525e395b 100644
--- a/theories/Core/Semantic/PER/Definitions.v
+++ b/theories/Core/Semantic/PER/Definitions.v
@@ -227,6 +227,34 @@ Section Per_univ_elem_ind_def.
   | i, a, b, R, H := per_univ_elem_ind' i a b R _.
 End Per_univ_elem_ind_def.
 
+Reserved Notation "'Sub' a <: b 'at' i" (in custom judg at level 90, a custom domain, b custom domain, i constr).
+
+Inductive per_subtyp : nat -> domain -> domain -> Prop :=
+| per_subtyp_neut :
+  `( {{ Dom b ≈ b' ∈ per_bot }} ->
+     {{ Sub ⇑ a b <: ⇑ a' b' at i }} )
+| per_subtyp_nat :
+  `( {{ Sub ℕ <: ℕ at i }} )
+| per_subtyp_univ :
+  `( i <= j ->
+     j < k ->
+     {{ Sub 𝕌@i <: 𝕌@j at k }} )
+| per_subtyp_pi :
+  `( forall (in_rel : relation domain) elem_rel elem_rel',
+        {{ DF a ≈ a' ∈ per_univ_elem i ↘ in_rel }} ->
+        (forall c c' b b',
+            {{ Dom c ≈ c' ∈ in_rel }} ->
+            {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+            {{ ⟦ B' ⟧ p' ↦ c' ↘ b' }} ->
+            {{ Sub b <: b' at i }}) ->
+        {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} ->
+        {{ DF Π a' p' B' ≈ Π a' p' B' ∈ per_univ_elem i ↘ elem_rel' }} ->
+        {{ Sub Π a p B <: Π a' p' B' at i }})
+where "'Sub' a <: b 'at' i" := (per_subtyp i a b) (in custom judg) : type_scope.
+
+#[export]
+ Hint Constructors per_subtyp : mcltt.
+
 (** 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'.
@@ -263,3 +291,26 @@ Definition valid_ctx : ctx -> Prop := fun Γ => per_ctx Γ Γ.
 Hint Transparent valid_ctx : mcltt.
 #[export]
 Hint Unfold valid_ctx : mcltt.
+
+Reserved Notation "'SubE' Γ <: Δ" (in custom judg at level 90, Γ custom exp, Δ custom exp).
+
+
+Inductive per_ctx_subtyp : ctx -> ctx -> Prop :=
+| per_ctx_subtyp_nil :
+  {{ SubE ⋅ <: ⋅ }}
+| per_ctx_subtyp_cons :
+  `{ forall tail_rel env_rel env_rel',
+        {{ SubE Γ <: Γ' }} ->
+        {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ tail_rel }} ->
+        (forall p p' a a'
+           (equiv_p_p' : {{ Dom p ≈ p' ∈ tail_rel }}),
+            {{ ⟦ A ⟧ p ↘ a }} ->
+            {{ ⟦ A' ⟧ p' ↘ a' }} ->
+            {{ Sub a <: a' at i }}) ->
+        {{ EF Γ , A ≈ Γ , A ∈ per_ctx_env ↘ env_rel }} ->
+        {{ EF Γ' , A' ≈ Γ' , A' ∈ per_ctx_env ↘ env_rel' }} ->
+        {{ SubE Γ, A <: Γ', A' }} }
+where "'SubE' Γ <: Δ" := (per_ctx_subtyp Γ Δ) (in custom judg) : type_scope.
+
+#[export]
+Hint Constructors per_ctx_subtyp : mcltt.
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
index de7efe87..8bf74077 100644
--- a/theories/Core/Semantic/PER/Lemmas.v
+++ b/theories/Core/Semantic/PER/Lemmas.v
@@ -615,6 +615,175 @@ Proof with mautosolve.
   assert (j <= max i j) by lia...
 Qed.
 
+Lemma per_subtyp_to_univ_elem : forall a b i,
+    {{ Sub a <: b at i }} ->
+    exists R R',
+      {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} /\
+        {{ DF b ≈ b ∈ per_univ_elem i ↘ R' }}.
+Proof.
+  destruct 1; do 2 eexists; mauto;
+    split; per_univ_elem_econstructor; mauto;
+    try apply Equivalence_Reflexive.
+  lia.
+Qed.
+
+
+Lemma PER_refl1 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R a a.
+Proof.
+  intros.
+  etransitivity; [eassumption |].
+  symmetry. assumption.
+Qed.
+
+Lemma PER_refl2 A (R : relation A) `(per : PER A R) : forall a b, R a b -> R b b.
+Proof.
+  intros. symmetry in H.
+  apply PER_refl1 in H;
+    auto.
+Qed.
+
+Ltac saturate_refl :=
+  repeat match goal with
+    | H : ?R ?a ?b |- _ =>
+        tryif unify a b
+        then fail
+        else
+          directed pose proof (PER_refl1 _ _ _ _ _ H);
+        directed pose proof (PER_refl2 _ _ _ _ _ H);
+        fail_if_dup
+    end.
+
+Ltac saturate_refl_for hd :=
+  repeat match goal with
+    | H : ?R ?a ?b |- _ =>
+        unify R hd;
+        tryif unify a b
+        then fail
+        else
+          directed pose proof (PER_refl1 _ _ _ _ _ H);
+        directed pose proof (PER_refl2 _ _ _ _ _ H);
+        fail_if_dup
+    end.
+
+Ltac solve_refl :=
+  solve [reflexivity || apply Equivalence_Reflexive].
+
+Lemma per_elem_subtyping : forall A B i,
+    {{ Sub A <: B at i }} ->
+    forall R R' a b,
+      {{ DF A ≈ A ∈ per_univ_elem i ↘ R }} ->
+      {{ DF B ≈ B ∈ per_univ_elem i ↘ R' }} ->
+      R a b ->
+      R' a b.
+Proof.
+  induction 1; intros.
+  all:handle_per_univ_elem_irrel;
+    (on_all_hyp: fun H => directed invert_per_univ_elem H);
+    apply_equiv_left;
+    trivial.
+  - firstorder mauto.
+  - intros.
+    handle_per_univ_elem_irrel.
+    assert (in_rel c c') by (apply_equiv_left; trivial).
+    assert (in_rel1 c c') by (apply_equiv_left; trivial).
+    destruct_rel_mod_eval.
+    destruct_rel_mod_app.
+    econstructor; eauto.
+    saturate_refl.
+    deepexec H1 ltac:(fun H => apply H).
+Qed.
+
+Lemma per_subtyp_refl1 : forall a b i R,
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ Sub a <: b at i }}.
+Proof.
+  simpl; induction 1 using per_univ_elem_ind;
+    subst;
+    mauto;
+    destruct_all.
+  assert ({{ DF Π A p B ≈ Π A' p' B' ∈ per_univ_elem i ↘ elem_rel }})
+    by (eapply per_univ_elem_pi'; eauto; intros; destruct_rel_mod_eval; mauto).
+  saturate_refl.
+  econstructor; eauto.
+  intros;
+      destruct_rel_mod_eval;
+      functional_eval_rewrite_clear;
+      trivial.
+Qed.
+
+Lemma per_subtyp_refl2 : forall a b i R,
+    {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} ->
+    {{ Sub b <: a at i }}.
+Proof.
+  intros.
+  symmetry in H.
+  eauto using per_subtyp_refl1.
+Qed.
+
+Lemma per_subtyp_trans : forall A1 A2 i,
+    {{ Sub A1 <: A2 at i }} ->
+    forall A3,
+      {{ Sub A2 <: A3 at i }} ->
+      {{ Sub A1 <: A3 at i }}.
+Proof.
+  induction 1; intros ? Hsub; simpl in *.
+  1-3:progressive_inversion;
+  mauto.
+  - econstructor; lia.
+  - dependent destruction Hsub.
+    handle_per_univ_elem_irrel.
+    econstructor; eauto.
+    + etransitivity; eassumption.
+    + intros.
+      saturate_refl.
+      directed invert_per_univ_elem H6.
+      directed invert_per_univ_elem H7.
+      destruct_rel_mod_eval.
+      functional_eval_rewrite_clear.
+      deepexec (H0 c c') ltac:(fun H => pose proof H).
+      deepexec (H5 c' c') ltac:(fun H => pose proof H);
+        [ apply_equiv_left; trivial |].
+      eauto.
+Qed.
+
+#[export]
+ Hint Resolve per_subtyp_trans : mcltt.
+
+#[export]
+  Instance per_subtyp_trans_ins i : Transitive (per_subtyp i).
+Proof.
+  eauto using per_subtyp_trans.
+Qed.
+
+Lemma per_subtyp_cumu : forall A1 A2 i,
+    {{ Sub A1 <: A2 at i }} ->
+    forall j,
+      i <= j ->
+      {{ Sub A1 <: A2 at j }}.
+Proof.
+  induction 1; intros; econstructor; mauto.
+  lia.
+Qed.
+
+#[export]
+ Hint Resolve per_subtyp_cumu : mcltt.
+
+Lemma per_subtyp_cumu_left : forall A1 A2 i j,
+    {{ Sub A1 <: A2 at i }} ->
+    {{ Sub A1 <: A2 at max i j }}.
+Proof.
+  intros. eapply per_subtyp_cumu; try eassumption.
+  lia.
+Qed.
+
+Lemma per_subtyp_cumu_right : forall A1 A2 i j,
+    {{ Sub A1 <: A2 at i }} ->
+    {{ Sub A1 <: A2 at max j i }}.
+Proof.
+  intros. eapply per_subtyp_cumu; try eassumption.
+  lia.
+Qed.
+
 Add Parametric Morphism : per_ctx_env
     with signature (@relation_equivalence env) ==> eq ==> eq ==> iff as per_ctx_env_morphism_iff.
 Proof with mautosolve.
@@ -891,3 +1060,109 @@ Proof.
   intros * [? H].
   induction H; simpl; congruence.
 Qed.
+
+Lemma per_ctx_subtyp_to_env : forall Γ Δ,
+    {{ SubE Γ <: Δ }} ->
+    exists R R',
+      {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ R }} /\
+        {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ R' }}.
+Proof.
+  destruct 1; destruct_all.
+  - repeat eexists; econstructor; apply Equivalence_Reflexive.
+  - eauto.
+Qed.
+
+Lemma per_ctx_env_subtyping : forall Γ Δ,
+    {{ SubE Γ <: Δ }} ->
+    forall R R' p p',
+      {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ R }} ->
+      {{ EF Δ ≈ Δ ∈ per_ctx_env ↘ R' }} ->
+      R p p' ->
+      R' p p'.
+Proof.
+  induction 1; intros.
+  all:handle_per_ctx_env_irrel;
+    (on_all_hyp: fun H => directed invert_per_ctx_env H);
+    apply_equiv_left;
+    trivial.
+
+  handle_per_ctx_env_irrel.
+  destruct_all.
+  deepexec IHper_ctx_subtyp ltac:(fun H => pose proof H).
+  deepexec H2 ltac:(fun H => destruct H as []).
+  deepexec H11 ltac:(fun H => destruct H as []).
+  deepexec H1 ltac:(fun H => pose proof H).
+  destruct (per_subtyp_to_univ_elem _ _ _ H15) as [? [? [? ?]]].
+  handle_per_univ_elem_irrel.
+  eexists; try eassumption.
+
+  eapply per_elem_subtyping with (i := max x (max i0 i)).
+  - eauto using per_subtyp_cumu_right.
+  - saturate_refl.
+    eauto using per_univ_elem_cumu_max_left.
+  - saturate_refl.
+    eauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
+  - trivial.
+Qed.
+
+Lemma per_ctx_subtyp_refl1 : forall Γ Δ R,
+    {{ EF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ SubE Γ <: Δ }}.
+Proof.
+  induction 1; mauto.
+
+  assert (exists R, {{ EF Γ , A ≈ Γ' , A' ∈ per_ctx_env ↘ R }}) by
+    (eexists; eapply @per_ctx_env_cons' with (i := i); eassumption).
+  destruct_all.
+  econstructor; try solve [saturate_refl; mauto 2].
+  intros.
+  unfold rel_typ in *.
+  destruct_rel_mod_eval.
+  simplify_evals.
+  eauto using per_subtyp_refl1.
+Qed.
+
+Lemma per_ctx_subtyp_refl2 : forall Γ Δ R,
+    {{ EF Γ ≈ Δ ∈ per_ctx_env ↘ R }} ->
+    {{ SubE Δ <: Γ }}.
+Proof.
+  intros. symmetry in H. eauto using per_ctx_subtyp_refl1.
+Qed.
+
+Lemma per_ctx_subtyp_trans : forall Γ1 Γ2,
+    {{ SubE Γ1 <: Γ2 }} ->
+    forall Γ3,
+      {{ SubE Γ2 <: Γ3 }} ->
+      {{ SubE Γ1 <: Γ3 }}.
+Proof.
+  induction 1; intros;
+    progressive_inversion;
+      mauto 1;
+      clear_PER.
+
+  handle_per_ctx_env_irrel.
+  econstructor; try eassumption.
+  - firstorder.
+  - instantiate (1 := max i i0).
+    intros.
+    cutexec per_ctx_env_subtyping H ltac:(fun H => deepexec H ltac:(fun H => pose proof H)).
+    cutexec per_ctx_env_subtyping H7 ltac:(fun H => deepexec H ltac:(fun H => pose proof H)).
+    deepexec H22 ltac:(fun H => destruct H as []).
+
+    etransitivity.
+    + saturate_refl_for tail_rel4.
+      apply_equiv_right.
+      deepexec (H1 p p) ltac:(fun H => eauto using per_subtyp_cumu_left, H).
+    + eapply per_subtyp_cumu_right.
+      eapply H9; eauto.
+      apply_equiv_left; trivial.
+Qed.
+
+#[export]
+ Hint Resolve per_ctx_subtyp_trans : mcltt.
+
+#[export]
+  Instance per_ctx_subtyp_trans_ins : Transitive per_ctx_subtyp.
+Proof.
+  eauto using per_ctx_subtyp_trans.
+Qed.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 8ed1439f..d1f5c4f6 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -266,12 +266,11 @@ Ltac deepexec lem tac :=
       exvar T ltac:(fun x =>
                       lazymatch type of T with
                       | Prop => match goal with
-                            | H : _ |- _ => unify x H
-                            | _ => idtac
+                            | H : _ |- _ => unify x H; deepexec constr:(lem x) tac
+                            | _ => deepexec constr:(lem x) tac
                             end
-                      | _ => idtac
-                      end;
-                      deepexec constr:(lem x) tac)
+                      | _ => deepexec constr:(lem x) tac
+                      end)
   | _ => tac lem
   end.
 
@@ -291,14 +290,13 @@ Ltac cutexec lem C tac :=
                         unify x C;
                         tac lem
                       else
-                        (lazymatch type of T with
+                        lazymatch type of T with
                          | Prop => match goal with
-                               | H : _ |- _ => unify x H
-                               | _ => idtac
+                               | H : _ |- _ => unify x H; cutexec constr:(lem x) C tac
+                               | _ => cutexec constr:(lem x) C tac
                                end
-                         | _ => idtac
-                         end;
-                         cutexec constr:(lem x) C tac))
+                         | _ => cutexec constr:(lem x) C tac
+                         end)
   | _ => tac lem
   end.
 
@@ -348,3 +346,11 @@ Ltac unify_args H P :=
 
 #[global]
   Ltac apply_equiv_right := repeat apply_equiv_right1.
+
+#[global]
+  Ltac clear_PER :=
+  repeat match goal with
+    | H : PER _ |- _ => clear H
+    | H : Symmetric _ |- _ => clear H
+    | H : Transitive _ |- _ => clear H
+    end.