diff --git a/_CoqProject b/_CoqProject
index c4c2f315..8a1b4d9a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -37,16 +37,18 @@ theories/LogicalRelation/ShapeView.v
 theories/LogicalRelation/Reflexivity.v
 theories/LogicalRelation/Irrelevance.v
 theories/LogicalRelation/Weakening.v
-theories/LogicalRelation/Universe.v
 theories/LogicalRelation/Neutral.v
 theories/LogicalRelation/Transitivity.v
 theories/LogicalRelation/InstKripke.v
 theories/LogicalRelation/EqRedRight.v
 theories/LogicalRelation/Reduction.v
 theories/LogicalRelation/NormalRed.v
-theories/LogicalRelation/Application.v
-theories/LogicalRelation/SimpleArr.v
-theories/LogicalRelation/Id.v
+theories/LogicalRelation/Introductions/Universe.v
+theories/LogicalRelation/Introductions/Poly.v
+theories/LogicalRelation/Introductions/Pi.v
+theories/LogicalRelation/Introductions/Application.v
+theories/LogicalRelation/Introductions/SimpleArr.v
+theories/LogicalRelation/Introductions/Id.v
 
 theories/Validity/Validity.v
 theories/Validity/Irrelevance.v
@@ -85,4 +87,4 @@ theories/Decidability/UntypedSoundness.v
 theories/Decidability/UntypedCompleteness.v
 theories/Decidability.v
 
-theories/Decidability/Execution.v
\ No newline at end of file
+theories/Decidability/Execution.v
diff --git a/theories/LogicalRelation/InstKripke.v b/theories/LogicalRelation/InstKripke.v
index ede13be9..ade78f56 100644
--- a/theories/LogicalRelation/InstKripke.v
+++ b/theories/LogicalRelation/InstKripke.v
@@ -1,7 +1,7 @@
 (** * LogRel.LogicalRelation.InstKripke: combinators to instantiate Kripke-style quantifications *)
 From Coq Require Import CRelationClasses.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction  Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed EqRedRight.
+From LogRel.LogicalRelation Require Import Induction  Escape Reflexivity Neutral Weakening Irrelevance Reduction Transitivity NormalRed EqRedRight.
 
 Set Universe Polymorphism.
 Set Printing Primitive Projection Parameters.
diff --git a/theories/LogicalRelation/Application.v b/theories/LogicalRelation/Introductions/Application.v
similarity index 100%
rename from theories/LogicalRelation/Application.v
rename to theories/LogicalRelation/Introductions/Application.v
diff --git a/theories/LogicalRelation/Id.v b/theories/LogicalRelation/Introductions/Id.v
similarity index 100%
rename from theories/LogicalRelation/Id.v
rename to theories/LogicalRelation/Introductions/Id.v
diff --git a/theories/LogicalRelation/Introductions/Pi.v b/theories/LogicalRelation/Introductions/Pi.v
new file mode 100644
index 00000000..6a86be81
--- /dev/null
+++ b/theories/LogicalRelation/Introductions/Pi.v
@@ -0,0 +1,47 @@
+From Coq Require Import ssrbool.
+From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
+From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Induction NormalRed EqRedRight.
+From LogRel.LogicalRelation.Introductions Require Import Poly.
+
+Set Universe Polymorphism.
+
+Section PolyRedPi.
+  Context `{GenericTypingProperties}.
+
+  Lemma LRPiPoly0 {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-Π<l> tProd A B].
+  Proof.
+    econstructor; tea; pose proof (polyRedId PAB) as []; escape.
+    + eapply redtywf_refl; gen_typing.
+    + unshelve eapply escapeEq; tea; eapply reflLRTyEq.
+    + eapply convty_prod; tea; unshelve eapply escapeEq; tea; eapply reflLRTyEq.
+  Defined.
+
+  Definition LRPiPoly {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-<l> tProd A B] := LRPi' (LRPiPoly0 PAB).
+
+  Lemma LRPiPolyEq0 {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
+    [Γ |- A'] -> [Γ ,, A' |- B'] ->
+    [Γ ||-Π tProd A B ≅ tProd A' B' | LRPiPoly0 PAB].
+  Proof.
+    econstructor; cbn; tea.
+    + eapply redtywf_refl; gen_typing.
+    + pose proof (polyRedEqId PAB Peq) as []; now escape.
+    + pose proof (polyRedEqId PAB Peq) as []; escape.
+      eapply convty_prod; tea.
+      eapply escape; now apply (polyRedId PAB).
+  Qed.
+
+  Lemma LRPiPolyEq {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
+    [Γ |- A'] -> [Γ ,, A' |- B'] ->
+    [Γ ||-<l> tProd A B ≅ tProd A' B' | LRPiPoly PAB].
+  Proof.
+    now eapply LRPiPolyEq0.
+  Qed.
+
+  Lemma LRPiPolyEq' {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') (RAB : [Γ ||-<l> tProd A B]):
+    [Γ |- A'] -> [Γ ,, A' |- B'] ->
+    [Γ ||-<l> tProd A B ≅ tProd A' B' | RAB].
+  Proof.
+    intros; irrelevanceRefl; now eapply LRPiPolyEq.
+  Qed.
+
+End PolyRedPi.
diff --git a/theories/LogicalRelation/Introductions/Poly.v b/theories/LogicalRelation/Introductions/Poly.v
new file mode 100644
index 00000000..5848ffcc
--- /dev/null
+++ b/theories/LogicalRelation/Introductions/Poly.v
@@ -0,0 +1,134 @@
+From Coq Require Import ssrbool.
+From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
+From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Transitivity EqRedRight InstKripke.
+
+Set Universe Polymorphism.
+
+Lemma subst_wk_id_tail Γ P t : P[t .: @wk_id Γ >> tRel] = P[t..].
+Proof. setoid_rewrite id_ren; now bsimpl. Qed.
+
+Set Printing Primitive Projection Parameters.
+
+Section PolyValidity.
+
+  Context `{GenericTypingProperties}.
+
+  Lemma mkPolyRed {Γ l A B} (wfΓ : [|-Γ])
+    (RA : forall Δ (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> A⟨ρ⟩])
+    (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> a ≅ b : _ | RA Δ ρ wfΔ] -> [Δ ||-<l> B[a .: ρ >> tRel]])
+    (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||-<l> a ≅ b : _ | RA Δ ρ wfΔ]),
+      [Δ ||-<l> B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) :
+    PolyRed Γ l A B.
+  Proof.
+    assert [Γ |- A] by (eapply escape; now eapply instKripke).
+    unshelve econstructor; tea.
+    unshelve epose proof (h := RB _ (tRel 0) (tRel 0) (@wk1 Γ A) _ _).
+    + gen_typing.
+    + eapply var0; tea; now rewrite wk1_ren_on.
+    + escape. now rewrite <- eq_id_subst_scons in Esch.
+  Qed.
+
+  Lemma mkPolyRed' {Γ l A B} (RA : [Γ ||-<l> A])
+    (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> a ≅ b : _ | wk ρ wfΔ RA] -> [Δ ||-<l> B[a .: ρ >> tRel]])
+    (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||-<l> a ≅ b : _ | wk ρ wfΔ RA]),
+      [Δ ||-<l> B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) :
+    PolyRed Γ l A B.
+  Proof.
+    unshelve eapply mkPolyRed; tea.
+    escape; gen_typing.
+  Qed.
+
+
+  Lemma polyCodSubstRed {Γ l F G} (RF : [Γ ||-<l> F]) :
+    PolyRed Γ l F G -> forall t u, [Γ ||-<l> t ≅ u : _ | RF] -> [Γ ||-<l> G[t..]].
+  Proof.
+    intros PFG ???.
+    assert (wfΓ : [|- Γ]) by (escape ; gen_typing).
+    erewrite <- subst_wk_id_tail.
+    eapply (PolyRed.posRed PFG wk_id wfΓ ).
+    irrelevance.
+  Qed.
+
+  Lemma polyCodSubstExtRed {Γ l F G} (RF : [Γ ||-<l> F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) :
+    forall t u (Rt : [Γ ||-<l> t ≅ u : _ | RF]),
+    [Γ ||-<l> G[t..] ≅ G[u..]| RG t u Rt].
+  Proof.
+    intros. assert (wfΓ : [|- Γ]) by (escape; gen_typing).
+    irrelevance0; erewrite <- subst_wk_id_tail; [reflexivity|].
+    unshelve eapply (PolyRed.posExt PFG wk_id wfΓ); irrelevance.
+  Qed.
+
+  Lemma polyRedId {Γ l F G} : PolyRed Γ l F G -> [Γ ||-<l> F] × [Γ ,, F ||-<l> G].
+  Proof.
+    intros PFG; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
+    split; [exact (instKripke wfΓ (PolyRed.shpRed PFG))| exact (instKripkeSubst wfΓ (PolyRed.posRed PFG))].
+  Qed.
+
+  Lemma polyRedEqId {Γ l F F' G G'} (PFG : PolyRed Γ l F G) (RFG := polyRedId PFG) :
+    PolyRedEq PFG F' G' -> [Γ ||-<l> F ≅ F' | fst RFG] × [Γ ,, F ||-<l> G ≅ G' | snd RFG].
+  Proof.
+    intros PFGeq; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
+    split.
+    - pose (instKripkeEq wfΓ (PolyRedEq.shpRed PFGeq)); irrelevance.
+    - unshelve epose proof (instKripkeSubstEq wfΓ  _).
+      7: intros; eapply LRTransEq; [|unshelve eapply (PolyRedEq.posRed PFGeq _ _ (urefl hab))];
+        try (unshelve eapply (PolyRed.posExt PFG); tea).
+      irrelevance.
+  Qed.
+
+  Lemma polyRedEqCodSubstExt {Γ l F F' G G'} (RF : [Γ ||-<l> F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) :
+    PolyRedEq PFG F' G' ->
+    forall t u (Rt : [Γ ||-<l> t ≅ u : _ | RF]),
+    [Γ ||-<l> G[t..] ≅ G'[u..]| RG t u Rt].
+  Proof.
+    intros Peq *; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
+    unshelve epose proof (h := posRedExt Peq wk_id wfΓ _).
+    3: irrelevance.
+    rewrite subst_wk_id_tail in h; irrelevance.
+  Qed.
+
+  Lemma polyRedSubst {Γ l A B t} (PAB : PolyRed Γ l A B)
+    (Rt : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
+      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> t[a .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
+    (Rtext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
+      [Δ ||-<l> a : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> t[a .: ρ >> tRel] ≅ t[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
+    : PolyRed Γ l A B[t]⇑.
+  Proof.
+    destruct PAB; opector; tea.
+    + intros; rewrite liftSubst_scons_eq.
+      unshelve eapply posRed; [..| eapply Rt]; tea ; now irrelevanceRefl.
+    + unshelve epose proof (posRed _ t t (@wk1 Γ A) _ _).
+      - escape; gen_typing.
+      - replace t with t[tRel 0 .: @wk1 Γ A >> tRel].
+        2:{ bsimpl; rewrite scons_eta'; now asimpl. }
+        eapply Rt.
+        eapply var0; tea; now rewrite wk1_ren_on.
+      - escape.
+        replace (B[_]) with B[t .: @wk1 Γ A >> tRel]; tea.
+        now setoid_rewrite wk1_ren.
+    + intros; irrelevance0; rewrite liftSubst_scons_eq;[reflexivity|].
+      unshelve eapply posExt; tea; eapply Rt + eapply Rtext; cbn; irrelevanceRefl.
+      1: now eapply lrefl.
+      1: now eapply urefl.
+      eassumption.
+  Qed.
+
+  Lemma polyRedEqSubst {Γ l A B t u} (PAB : PolyRed Γ l A B)
+    (Rtu : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
+      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
+      [Δ ||-<l> t[a .: ρ >> tRel] ≅ u[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
+    (PABt : PolyRed Γ l A B[t]⇑)
+    : PolyRedEq PABt A B[u]⇑.
+  Proof.
+    constructor.
+    - intros; eapply reflLRTyEq.
+    - intros; irrelevance0; rewrite liftSubst_scons_eq; [reflexivity|].
+      unshelve eapply PolyRed.posExt; cycle 1; tea.
+      eapply Rtu; irrelevanceRefl; now eapply lrefl.
+  Qed.
+
+End PolyValidity.
diff --git a/theories/LogicalRelation/SimpleArr.v b/theories/LogicalRelation/Introductions/SimpleArr.v
similarity index 96%
rename from theories/LogicalRelation/SimpleArr.v
rename to theories/LogicalRelation/Introductions/SimpleArr.v
index 0e1a7853..c784570b 100644
--- a/theories/LogicalRelation/SimpleArr.v
+++ b/theories/LogicalRelation/Introductions/SimpleArr.v
@@ -1,5 +1,6 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Transitivity Application.
+From LogRel.LogicalRelation.Introductions Require Import Poly Pi.
 
 Set Universe Polymorphism.
 Set Printing Primitive Projection Parameters.
@@ -24,14 +25,8 @@ Section SimpleArrow.
 
   Lemma ArrRedTy0 {Γ l A B} : [Γ ||-<l> A] -> [Γ ||-<l> B] -> [Γ ||-Π<l> arr A B].
   Proof.
-    intros RA RB; escape.
-    unshelve econstructor; [exact A| exact B⟨↑⟩|..]; tea.
-    - eapply redtywf_refl.
-      now eapply wft_simple_arr.
-    - now unshelve eapply escapeEq, reflLRTyEq.
-    - eapply convty_simple_arr; tea.
-      all: now unshelve eapply escapeEq, reflLRTyEq.
-    - now eapply shiftPolyRed.
+    intros RA RB.
+    now apply LRPiPoly0, shiftPolyRed.
   Qed.
 
   Lemma ArrRedTy {Γ l A B} : [Γ ||-<l> A] -> [Γ ||-<l> B] -> [Γ ||-<l> arr A B].
diff --git a/theories/LogicalRelation/Universe.v b/theories/LogicalRelation/Introductions/Universe.v
similarity index 100%
rename from theories/LogicalRelation/Universe.v
rename to theories/LogicalRelation/Introductions/Universe.v
diff --git a/theories/TypingProperties/LogRelConsequences.v b/theories/TypingProperties/LogRelConsequences.v
index e6df5606..2392c412 100644
--- a/theories/TypingProperties/LogRelConsequences.v
+++ b/theories/TypingProperties/LogRelConsequences.v
@@ -4,6 +4,7 @@ From LogRel.TypingProperties Require Import PropertiesDefinition DeclarativeProp
 
 From LogRel Require Import LogicalRelation Fundamental.
 From LogRel.LogicalRelation Require Import Escape Irrelevance Transitivity Neutral Induction NormalRed.
+From LogRel.LogicalRelation.Introductions Require Import Poly.
 From LogRel.Validity Require Import Validity Escape Poly Irrelevance.
 
 (** ** Stability of typing under substitution *)
diff --git a/theories/Validity/Introductions/Pi.v b/theories/Validity/Introductions/Pi.v
index 206e3a12..94dc0b6b 100644
--- a/theories/Validity/Introductions/Pi.v
+++ b/theories/Validity/Introductions/Pi.v
@@ -1,53 +1,11 @@
 From Coq Require Import ssrbool.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Induction NormalRed EqRedRight.
+From LogRel.LogicalRelation.Introductions Require Import Poly Pi.
 From LogRel.Validity Require Import Validity Irrelevance Properties SingleSubst Reflexivity Universe Poly.
 
 Set Universe Polymorphism.
 
-
-Section PolyRedPi.
-  Context `{GenericTypingProperties}.
-
-  Lemma LRPiPoly0 {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-Π<l> tProd A B].
-  Proof.
-    econstructor; tea; pose proof (polyRedId PAB) as []; escape.
-    + eapply redtywf_refl; gen_typing.
-    + unshelve eapply escapeEq; tea; eapply reflLRTyEq.
-    + eapply convty_prod; tea; unshelve eapply escapeEq; tea; eapply reflLRTyEq.
-  Defined.
-
-  Definition LRPiPoly {Γ l A B} (PAB : PolyRed Γ l A B) : [Γ ||-<l> tProd A B] := LRPi' (LRPiPoly0 PAB).
-
-  Lemma LRPiPolyEq0 {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
-    [Γ |- A'] -> [Γ ,, A' |- B'] ->
-    [Γ ||-Π tProd A B ≅ tProd A' B' | LRPiPoly0 PAB].
-  Proof.
-    econstructor; cbn; tea.
-    + eapply redtywf_refl; gen_typing.
-    + pose proof (polyRedEqId PAB Peq) as []; now escape.
-    + pose proof (polyRedEqId PAB Peq) as []; escape.
-      eapply convty_prod; tea.
-      eapply escape; now apply (polyRedId PAB).
-  Qed.
-
-  Lemma LRPiPolyEq {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') :
-    [Γ |- A'] -> [Γ ,, A' |- B'] ->
-    [Γ ||-<l> tProd A B ≅ tProd A' B' | LRPiPoly PAB].
-  Proof.
-    now eapply LRPiPolyEq0.
-  Qed.
-
-  Lemma LRPiPolyEq' {Γ l A A' B B'} (PAB : PolyRed Γ l A B) (Peq : PolyRedEq PAB A' B') (RAB : [Γ ||-<l> tProd A B]):
-    [Γ |- A'] -> [Γ ,, A' |- B'] ->
-    [Γ ||-<l> tProd A B ≅ tProd A' B' | RAB].
-  Proof.
-    intros; irrelevanceRefl; now eapply LRPiPolyEq.
-  Qed.
-
-End PolyRedPi.
-
-
 Section PiTyValidity.
 
   Context `{GenericTypingProperties}.
diff --git a/theories/Validity/Introductions/Poly.v b/theories/Validity/Introductions/Poly.v
index f32b33d1..f9e71e73 100644
--- a/theories/Validity/Introductions/Poly.v
+++ b/theories/Validity/Introductions/Poly.v
@@ -1,6 +1,7 @@
 From Coq Require Import ssrbool.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance Transitivity EqRedRight InstKripke.
+From LogRel.LogicalRelation.Introductions Require Import Poly.
 From LogRel.Validity Require Import Validity Irrelevance Properties Reflexivity Universe.
 
 Set Universe Polymorphism.
@@ -15,133 +16,12 @@ Proof.
   bsimpl ; now substify.
 Qed.
 
-Lemma subst_wk_id_tail Γ P t : P[t .: @wk_id Γ >> tRel] = P[t..].
-Proof. setoid_rewrite id_ren; now bsimpl. Qed.
-
 Set Printing Primitive Projection Parameters.
 
 Section PolyValidity.
 
   Context `{GenericTypingProperties}.
 
-  Lemma mkPolyRed {Γ l A B} (wfΓ : [|-Γ])
-    (RA : forall Δ (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> A⟨ρ⟩])
-    (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> a ≅ b : _ | RA Δ ρ wfΔ] -> [Δ ||-<l> B[a .: ρ >> tRel]])
-    (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||-<l> a ≅ b : _ | RA Δ ρ wfΔ]),
-      [Δ ||-<l> B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) :
-    PolyRed Γ l A B.
-  Proof.
-    assert [Γ |- A] by (eapply escape; now eapply instKripke).
-    unshelve econstructor; tea.
-    unshelve epose proof (h := RB _ (tRel 0) (tRel 0) (@wk1 Γ A) _ _).
-    + gen_typing.
-    + eapply var0; tea; now rewrite wk1_ren_on.
-    + escape. now rewrite <- eq_id_subst_scons in Esch.
-  Qed.
-
-  Lemma mkPolyRed' {Γ l A B} (RA : [Γ ||-<l> A])
-    (RB : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]), [Δ ||-<l> a ≅ b : _ | wk ρ wfΔ RA] -> [Δ ||-<l> B[a .: ρ >> tRel]])
-    (RBext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|- Δ]) (Rab : [Δ ||-<l> a ≅ b : _ | wk ρ wfΔ RA]),
-      [Δ ||-<l> B[a .: ρ >> tRel] ≅ B[b .: ρ >> tRel] | RB Δ a b ρ wfΔ Rab]) :
-    PolyRed Γ l A B.
-  Proof.
-    unshelve eapply mkPolyRed; tea.
-    escape; gen_typing.
-  Qed.
-
-
-  Lemma polyCodSubstRed {Γ l F G} (RF : [Γ ||-<l> F]) :
-    PolyRed Γ l F G -> forall t u, [Γ ||-<l> t ≅ u : _ | RF] -> [Γ ||-<l> G[t..]].
-  Proof.
-    intros PFG ???.
-    assert (wfΓ : [|- Γ]) by (escape ; gen_typing).
-    erewrite <- subst_wk_id_tail.
-    eapply (PolyRed.posRed PFG wk_id wfΓ ).
-    irrelevance.
-  Qed.
-
-  Lemma polyCodSubstExtRed {Γ l F G} (RF : [Γ ||-<l> F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) :
-    forall t u (Rt : [Γ ||-<l> t ≅ u : _ | RF]),
-    [Γ ||-<l> G[t..] ≅ G[u..]| RG t u Rt].
-  Proof.
-    intros. assert (wfΓ : [|- Γ]) by (escape; gen_typing).
-    irrelevance0; erewrite <- subst_wk_id_tail; [reflexivity|].
-    unshelve eapply (PolyRed.posExt PFG wk_id wfΓ); irrelevance.
-  Qed.
-
-  Lemma polyRedId {Γ l F G} : PolyRed Γ l F G -> [Γ ||-<l> F] × [Γ ,, F ||-<l> G].
-  Proof.
-    intros PFG; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
-    split; [exact (instKripke wfΓ (PolyRed.shpRed PFG))| exact (instKripkeSubst wfΓ (PolyRed.posRed PFG))].
-  Qed.
-
-  Lemma polyRedEqId {Γ l F F' G G'} (PFG : PolyRed Γ l F G) (RFG := polyRedId PFG) :
-    PolyRedEq PFG F' G' -> [Γ ||-<l> F ≅ F' | fst RFG] × [Γ ,, F ||-<l> G ≅ G' | snd RFG].
-  Proof.
-    intros PFGeq; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
-    split.
-    - pose (instKripkeEq wfΓ (PolyRedEq.shpRed PFGeq)); irrelevance.
-    - unshelve epose proof (instKripkeSubstEq wfΓ  _).
-      7: intros; eapply LRTransEq; [|unshelve eapply (PolyRedEq.posRed PFGeq _ _ (urefl hab))];
-        try (unshelve eapply (PolyRed.posExt PFG); tea).
-      irrelevance.
-  Qed.
-
-  Lemma polyRedEqCodSubstExt {Γ l F F' G G'} (RF : [Γ ||-<l> F]) (PFG : PolyRed Γ l F G) (RG := polyCodSubstRed RF PFG) :
-    PolyRedEq PFG F' G' ->
-    forall t u (Rt : [Γ ||-<l> t ≅ u : _ | RF]),
-    [Γ ||-<l> G[t..] ≅ G'[u..]| RG t u Rt].
-  Proof.
-    intros Peq *; assert (wfΓ : [|- Γ]) by (destruct PFG; gen_typing).
-    unshelve epose proof (h := posRedExt Peq wk_id wfΓ _).
-    3: irrelevance.
-    rewrite subst_wk_id_tail in h; irrelevance.
-  Qed.
-
-  Lemma polyRedSubst {Γ l A B t} (PAB : PolyRed Γ l A B)
-    (Rt : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
-      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
-      [Δ ||-<l> t[a .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
-    (Rtext : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
-      [Δ ||-<l> a : _ | PolyRed.shpRed PAB ρ wfΔ] ->
-      [Δ ||-<l> b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
-      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
-      [Δ ||-<l> t[a .: ρ >> tRel] ≅ t[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
-    : PolyRed Γ l A B[t]⇑.
-  Proof.
-    destruct PAB; opector; tea.
-    + intros; rewrite liftSubst_scons_eq.
-      unshelve eapply posRed; [..| eapply Rt]; tea ; now irrelevanceRefl.
-    + unshelve epose proof (posRed _ t t (@wk1 Γ A) _ _).
-      - escape; gen_typing.
-      - replace t with t[tRel 0 .: @wk1 Γ A >> tRel].
-        2:{ bsimpl; rewrite scons_eta'; now asimpl. }
-        eapply Rt.
-        eapply var0; tea; now rewrite wk1_ren_on.
-      - escape.
-        replace (B[_]) with B[t .: @wk1 Γ A >> tRel]; tea.
-        now setoid_rewrite wk1_ren.
-    + intros; irrelevance0; rewrite liftSubst_scons_eq;[reflexivity|].
-      unshelve eapply posExt; tea; eapply Rt + eapply Rtext; cbn; irrelevanceRefl.
-      1: now eapply lrefl.
-      1: now eapply urefl.
-      eassumption.
-  Qed.
-
-  Lemma polyRedEqSubst {Γ l A B t u} (PAB : PolyRed Γ l A B)
-    (Rtu : forall Δ a b (ρ : Δ ≤ Γ) (wfΔ : [|-Δ]),
-      [Δ ||-<l> a ≅ b : _ | PolyRed.shpRed PAB ρ wfΔ] ->
-      [Δ ||-<l> t[a .: ρ >> tRel] ≅ u[b .: ρ >> tRel] : _ | PolyRed.shpRed PAB ρ wfΔ ])
-    (PABt : PolyRed Γ l A B[t]⇑)
-    : PolyRedEq PABt A B[u]⇑.
-  Proof.
-    constructor.
-    - intros; eapply reflLRTyEq.
-    - intros; irrelevance0; rewrite liftSubst_scons_eq; [reflexivity|].
-      unshelve eapply PolyRed.posExt; cycle 1; tea.
-      eapply Rtu; irrelevanceRefl; now eapply lrefl.
-  Qed.
-
   Context {l Γ F G} (VΓ : [||-v Γ])
     (VF : [Γ ||-v< l > F | VΓ ])
     (VG : [Γ ,, F ||-v< l > G | validSnoc VΓ VF]).
diff --git a/theories/Validity/Introductions/Sigma.v b/theories/Validity/Introductions/Sigma.v
index e860c78d..475da557 100644
--- a/theories/Validity/Introductions/Sigma.v
+++ b/theories/Validity/Introductions/Sigma.v
@@ -1,6 +1,7 @@
 From Coq Require Import ssrbool CRelationClasses.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Irrelevance Weakening Neutral Transitivity Reduction Application Universe EqRedRight SimpleArr NormalRed InstKripke.
+From LogRel.LogicalRelation.Introductions Require Import Poly.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion SingleSubst Reflexivity Reduction Universe Poly.