diff --git a/theories/Fundamental.v b/theories/Fundamental.v
index cc8653e..b344c07 100644
--- a/theories/Fundamental.v
+++ b/theories/Fundamental.v
@@ -150,7 +150,7 @@ Section Fundamental.
     econstructor.
     unshelve eapply (PiValid VΓ).
     - assumption.
-    - now eapply irrelevanceValidity.
+    - now eapply irrelevanceTy.
   Qed.
 
   Lemma FundTyUniv (Γ : context) (A : term)
@@ -236,7 +236,7 @@ Section Fundamental.
     FundTyEq Γ A B -> FundTyEq Γ B A.
   Proof.
     intros * [];  unshelve econstructor; tea.
-    now eapply symValidEq.
+    now eapply symValidTyEq.
   Qed.
 
   Lemma FundTyEqTrans : forall (Γ : context) (A B C : term),
@@ -245,7 +245,7 @@ Section Fundamental.
     FundTyEq Γ A C.
   Proof.
     intros * [] []; unshelve econstructor; tea. 1:irrValid.
-    eapply transValidEq; irrValid.
+    eapply transValidTyEq; irrValid.
     Unshelve. tea.
   Qed.
 
@@ -332,13 +332,13 @@ Section Fundamental.
     { eapply irrelevanceLift; [tea|]; irrValid. }
     assert (Vλt : [Γ ||-v< one > tLambda A' t : tProd A B | VΓ | VΠAB ]).
     { eapply conv; [|eapply lamValid].
-      + eapply symValidEq, PiCong; tea; try irrValid.
+      + eapply symValidTyEq, PiCong; tea; try irrValid.
         eapply reflValidTy.
       + eapply irrelevanceTmLift; irrValid.
     }
     assert (Vλu : [Γ ||-v< one > tLambda A'' u : tProd A B | VΓ | VΠAB ]).
     { eapply conv; [|eapply lamValid].
-      + eapply symValidEq, PiCong; tea; try irrValid.
+      + eapply symValidTyEq, PiCong; tea; try irrValid.
         eapply reflValidTy.
       + eapply irrelevanceTmLift; irrValid.
     }
@@ -363,7 +363,7 @@ Section Fundamental.
     + eapply irrelevanceTmEq'; [eapply eq0|].
       eapply transValidTmEq; [eapply betaValid|]; refold.
       - eapply irrelevanceTm'.
-        2: eapply (wkTmValid  (A := B)) with (ρ := wk_up A' (@wk1 Γ A)).
+        2: eapply (wkValidTm  (A := B)) with (ρ := wk_up A' (@wk1 Γ A)).
         * now bsimpl.
         * eapply irrelevanceTmLift; irrValid.
       - eapply irrelevanceTmEq'; [symmetry; eapply eq0|].
@@ -374,7 +374,7 @@ Section Fundamental.
     + apply symValidTmEq; eapply irrelevanceTmEq'; [eapply eq0|].
       eapply transValidTmEq; [eapply betaValid|]; refold.
       - eapply irrelevanceTm'.
-        2: eapply (wkTmValid  (A := B)) with (ρ := wk_up A'' (@wk1 Γ A)).
+        2: eapply (wkValidTm  (A := B)) with (ρ := wk_up A'' (@wk1 Γ A)).
         * now bsimpl.
         * eapply irrelevanceTmLift; irrValid.
       - eapply irrelevanceTmEq'; [symmetry; eapply eq0|].
@@ -384,16 +384,16 @@ Section Fundamental.
         apply reflValidTm; tea.
     Unshelve.
     all: refold; try irrValid.
-    * unshelve eapply irrelevanceValidity; tea.
+    * unshelve eapply irrelevanceTy; tea.
       rewrite <- (wk_up_wk1_ren_on Γ A' A).
-      eapply wkValid, irrelevanceLift; irrValid.
-    * eapply conv; [now eapply irrelevanceEq, wk1ValidTyEq|].
+      eapply wkValidTy, irrelevanceLift; irrValid.
+    * eapply conv; [now eapply irrelevanceTyEq, wk1ValidTyEq|].
       eapply irrelevanceTm'; [symmetry; eapply wk1_ren_on|].
       eapply var0Valid'.
-    * eapply irrelevanceValidity.
+    * eapply irrelevanceTy.
       rewrite <- (wk_up_wk1_ren_on Γ A'' A).
-      eapply wkValid, irrelevanceLift; irrValid.
-    * eapply conv; [now eapply irrelevanceEq, wk1ValidTyEq|].
+      eapply wkValidTy, irrelevanceLift; irrValid.
+    * eapply conv; [now eapply irrelevanceTyEq, wk1ValidTyEq|].
       eapply irrelevanceTm'; [symmetry; eapply wk1_ren_on|].
       eapply var0Valid'.
   Unshelve.
@@ -411,29 +411,29 @@ Section Fundamental.
   { now eapply PiValidDom. }
   assert (VΓA := validSnoc VΓ VA).
   assert (VΓAA : [Γ,, A ||-v< one > A⟨@wk1 Γ A⟩ | VΓA]).
-  { now eapply irrelevanceValidity, wk1ValidTy. }
+  { now eapply irrelevanceTy, wk1ValidTy. }
   assert (VΓAA0 : VAdequate (ta := ta) (Γ,, A,, A⟨@wk1 Γ A⟩) VR).
   { now eapply validSnoc. }
   assert (VΓAA' : [Γ,, A ||-v< one > A⟨↑⟩ | VΓA]).
   { now rewrite wk1_ren_on in VΓAA. }
   assert [Γ,, A ||-v< one > B | VΓA].
-  { eapply irrelevanceValidity, PiValidCod. }
+  { eapply irrelevanceTy, PiValidCod. }
   assert ([Γ,, A ||-v< one > tProd A⟨@wk1 Γ A⟩ B⟨upRen_term_term ↑⟩ | VΓA]).
   { rewrite <- (wk_up_wk1_ren_on Γ A A).
-    now eapply irrelevanceValidity, (wk1ValidTy (A := tProd A B)). }
+    now eapply irrelevanceTy, (wk1ValidTy (A := tProd A B)). }
   assert ([Γ,, A ||-v< one > tRel 0 : A⟨wk1 A⟩ | VΓA | VΓAA]).
   { eapply irrelevanceTm'; [rewrite wk1_ren_on; reflexivity|].
     unshelve apply var0Valid'. }
   assert ([(Γ,, A),, A⟨wk1 A⟩ ||-v< one > tProd A⟨↑⟩⟨↑⟩ B⟨upRen_term_term ↑⟩⟨upRen_term_term ↑⟩ | VΓAA0]).
   { assert (eq1 : (tProd A B)⟨@wk1 Γ A⟩⟨@wk1 (Γ,, A) A⟨@wk1 Γ A⟩⟩ = tProd (A⟨↑⟩⟨↑⟩) (B⟨upRen_term_term ↑⟩⟨upRen_term_term ↑⟩)).
     { rewrite wk1_ren_on, wk1_ren_on; reflexivity. }
-    eapply irrelevanceValidity'; [|eapply eq1|reflexivity].
-    now eapply wkValid, wkValid. }
+    eapply irrelevanceTy'; [|eapply eq1|reflexivity].
+    now eapply wkValidTy, wkValidTy. }
   assert ([Γ ||-v< one > tLambda A (tApp f⟨↑⟩ (tRel 0)) : tProd A B | VΓ | VΠ]).
   { eapply irrelevanceTm, lamValid.
     eapply irrelevanceTm'; [apply eq0|eapply (appValid (F := A⟨@wk1 Γ A⟩))].
     rewrite <- (wk1_ren_on Γ A).
-    eapply irrelevanceTm'; [|now eapply wkTmValid].
+    eapply irrelevanceTm'; [|now eapply wkValidTm].
     rewrite <- (wk_up_wk1_ren_on Γ A A).
     reflexivity. }
   Unshelve. all: try irrValid.
@@ -449,7 +449,7 @@ Section Fundamental.
     { rewrite wk1_ren_on, wk1_ren_on; reflexivity. }
     eapply irrelevanceTm'; [eapply eq1|].
     rewrite <- (wk1_ren_on (Γ,, A)  A⟨@wk1 Γ A⟩).
-    now eapply wkTmValid, wkTmValid.
+    now eapply wkValidTm, wkValidTm.
   + refold.
     match goal with |- [_ ||-v< _ > ?t ≅ ?u : _ | _ | _ ] => assert (Hrw : t = u) end.
     { rewrite <- eq0; now bsimpl. }
@@ -461,18 +461,18 @@ Section Fundamental.
     now rewrite <- (wk_up_wk1_ren_on Γ A A).
   Unshelve.
   all: refold; try irrValid.
-  { unshelve eapply irrelevanceValidity; [tea|].
+  { unshelve eapply irrelevanceTy; [tea|].
     rewrite <- (wk_up_wk1_ren_on Γ A A).
-    now eapply wkValid. }
-  { eapply (irrelevanceValidity' (A := A⟨↑⟩⟨@wk1 (Γ,, A) A⟨@wk1 Γ A⟩⟩)); [|now rewrite wk1_ren_on|reflexivity].
-    now eapply wkValid. }
+    now eapply wkValidTy. }
+  { eapply (irrelevanceTy' (A := A⟨↑⟩⟨@wk1 (Γ,, A) A⟨@wk1 Γ A⟩⟩)); [|now rewrite wk1_ren_on|reflexivity].
+    now eapply wkValidTy. }
   { eapply (irrelevanceTm' (A := A⟨@wk1 Γ A⟩⟨↑⟩)); [now rewrite wk1_ren_on|].
     apply var0Valid'. }
   Unshelve.
   all: try irrValid.
   { shelve. }
   { rewrite <- (wk1_ren_on (Γ,, A)  A⟨@wk1 Γ A⟩).
-    now eapply wkValid. }
+    now eapply wkValidTy. }
   Qed.
 
   Lemma FundTmEqFunExt : forall (Γ : context) (f g A B : term),
@@ -487,7 +487,7 @@ Section Fundamental.
     1:{
       eapply conv. 
       2: irrValid.
-      eapply symValidEq. eapply PiCong.
+      eapply symValidTyEq. eapply PiCong.
       eapply irrelevanceLift. 
       1,3,4: eapply reflValidTy.
       irrValid.
@@ -624,7 +624,7 @@ Section Fundamental.
     2: eapply natElimValid; irrValid.
     + eapply conv.
       2: eapply irrelevanceTm; now eapply natElimValid.
-      eapply symValidEq. 
+      eapply symValidTyEq. 
       eapply substSEq; tea. 
       2,3: irrValid.
       eapply reflValidTy.
@@ -682,7 +682,7 @@ Section Fundamental.
     2: eapply emptyElimValid; irrValid.
     + eapply conv.
       2: eapply irrelevanceTm; now eapply emptyElimValid.
-      eapply symValidEq.
+      eapply symValidTyEq.
       eapply substSEq; tea.
       2,3: irrValid.
       eapply reflValidTy.
@@ -837,7 +837,7 @@ Section Fundamental.
     3,5: unshelve eapply pairSndValid; irrValid.
     + tea.
     + eapply conv; tea.
-      eapply irrelevanceEq.
+      eapply irrelevanceTyEq.
       eapply substSEq.
       1,3: eapply reflValidTy.
       1: irrValid.
@@ -916,7 +916,7 @@ Section Fundamental.
     3: eapply conv.
     2,4: eapply reflValid; try irrValid.
     2: eapply conv; irrValid.
-    2: eapply symValidEq; eapply IdCongValid; tea; try irrValid.
+    2: eapply symValidTyEq; eapply IdCongValid; tea; try irrValid.
     eapply IdValid; irrValid.
     Unshelve. all: try eapply IdValid; try irrValid; eapply conv; irrValid.
     Unshelve. all: irrValid.
@@ -956,7 +956,7 @@ Section Fundamental.
     3,4: eapply IdValid; irrValid.
     1: eapply validSnoc; now eapply idElimMotiveCtxIdValid.
     eapply convCtx2'; tea.
-    1: eapply convCtx1; tea; [eapply symValidEq; irrValid| ].
+    1: eapply convCtx1; tea; [eapply symValidTyEq; irrValid| ].
     1,3: now eapply idElimMotiveCtxIdValid.
     eapply idElimMotiveCtxIdCongValid; tea; irrValid.
     Unshelve.
diff --git a/theories/Substitution/Conversion.v b/theories/Substitution/Conversion.v
index 07f5a2e..2094821 100644
--- a/theories/Substitution/Conversion.v
+++ b/theories/Substitution/Conversion.v
@@ -125,11 +125,11 @@ Lemma convCtx1 {Γ A B P l}
   [_ ||-v<l> P | VΓB].
 Proof.
   opector; intros.
-  - eapply validTy; tea; eapply convSubstCtx1; tea; now eapply symValidEq.
+  - eapply validTy; tea; eapply convSubstCtx1; tea; now eapply symValidTyEq.
   - irrelevanceRefl; unshelve eapply validTyExt.
     3,4: tea. 
-    1,2:  eapply convSubstCtx1; tea; now eapply symValidEq.
-    eapply convSubstEqCtx1; cycle 2; tea; now eapply symValidEq.
+    1,2:  eapply convSubstCtx1; tea; now eapply symValidTyEq.
+    eapply convSubstEqCtx1; cycle 2; tea; now eapply symValidTyEq.
     Unshelve. all: tea.
 Qed.
 
@@ -148,7 +148,7 @@ Proof.
   constructor; intros; irrelevanceRefl.
   eapply validTyEq; tea.
   Unshelve. 1: tea. 
-  unshelve eapply convSubstCtx1; cycle 5; tea; now eapply symValidEq.
+  unshelve eapply convSubstCtx1; cycle 5; tea; now eapply symValidTyEq.
 Qed.
 
 Lemma convSubstCtx2 {Γ Δ A1 B1 A2 B2 l σ} 
@@ -288,8 +288,8 @@ Lemma convCtx2 {Γ A1 B1 A2 B2 P l}
   [_ ||-v<l> P | VΓB12].
 Proof.
   assert [_ ||-v<l> A2 | VΓB1] by now eapply convCtx1.
-  assert [_ ||-v<l> B1 ≅ A1 | _ | VB1] by now eapply symValidEq.
-  assert [_ ||-v<l> B2 ≅ A2 | _ | VB2'] by (eapply convEqCtx1; tea; now eapply symValidEq).
+  assert [_ ||-v<l> B1 ≅ A1 | _ | VB1] by now eapply symValidTyEq.
+  assert [_ ||-v<l> B2 ≅ A2 | _ | VB2'] by (eapply convEqCtx1; tea; now eapply symValidTyEq).
   opector; intros.
   - eapply validTy; tea; now eapply convSubstCtx2'.
   - irrelevanceRefl; unshelve eapply validTyExt.
@@ -315,7 +315,7 @@ Lemma convCtx2' {Γ A1 A2 B1 B2 P l}
   (VP : [_ ||-v<l> P | VΓA12]) :
   [_ ||-v<l> P | VΓB12].
 Proof.
-  eapply irrelevanceValidity; eapply convCtx2; irrValid.
+  eapply irrelevanceTy; eapply convCtx2; irrValid.
   Unshelve. all: tea; irrValid.
 Qed.
 
diff --git a/theories/Substitution/Introductions/Id.v b/theories/Substitution/Introductions/Id.v
index db61d0e..1c17324 100644
--- a/theories/Substitution/Introductions/Id.v
+++ b/theories/Substitution/Introductions/Id.v
@@ -547,7 +547,7 @@ Context `{GenericTypingProperties}.
       1: eapply reflValidTy.
       now eapply reflValidTm.
     }
-    eapply transValidEq.
+    eapply transValidTyEq.
     - eapply substExtIdElimMotive.
       2: tea. all: tea.
       Unshelve. eapply substIdElimMotive; cycle 1; tea.
@@ -655,7 +655,7 @@ Context `{GenericTypingProperties}.
     assert (VPalt' : [_ ||-v<l> P' | VΓext']).
     1:{
       eapply convCtx2'; tea.
-      1: eapply convCtx1; tea; [now eapply symValidEq| ].
+      1: eapply convCtx1; tea; [now eapply symValidTyEq| ].
       1,3: now eapply idElimMotiveCtxIdValid.
       eapply idElimMotiveCtxIdCongValid; tea.
       Unshelve. 1: now eapply idElimMotiveCtxIdValid. tea.
@@ -696,7 +696,7 @@ Context `{GenericTypingProperties}.
       6,7: tea.  5-8: tea. 2-4: tea. 1: tea.
       2: eapply conv.
       1,3: now eapply reflValid.
-      1: eapply symValidEq; now eapply IdCongValid.
+      1: eapply symValidTyEq; now eapply IdCongValid.
       now eapply reflCongValid.
       Unshelve. all: now eapply IdValid.
     + eapply LRTmRedConv; tea.
@@ -730,7 +730,7 @@ Context `{GenericTypingProperties}.
       1: now eapply reflValid.
       eapply reflCongValid; tea.
       eapply conv; tea.
-      now eapply symValidEq.
+      now eapply symValidTyEq.
       Unshelve. now eapply IdValid.
     }
     eapply redwfSubstValid; cycle 1.
diff --git a/theories/Substitution/Introductions/Nat.v b/theories/Substitution/Introductions/Nat.v
index d6fa627..9b78283 100644
--- a/theories/Substitution/Introductions/Nat.v
+++ b/theories/Substitution/Introductions/Nat.v
@@ -544,7 +544,7 @@ Lemma elimSuccHypTyCongValid {Γ l P P'}
     [Γ ||-v<l> elimSuccHypTy P ≅ elimSuccHypTy P' | VΓ | elimSuccHypTyValid VΓ VP].
   Proof.
     unfold elimSuccHypTy.
-    eapply irrelevanceEq.
+    eapply irrelevanceTyEq.
     assert [Γ,, tNat ||-v< l > P'[tSucc (tRel 0)]⇑ | validSnoc VΓ VN]. 1:{
       eapply substLiftS; tea.
       eapply irrelevanceTm.
diff --git a/theories/Substitution/Introductions/Pi.v b/theories/Substitution/Introductions/Pi.v
index 2babc95..db0bd22 100644
--- a/theories/Substitution/Introductions/Pi.v
+++ b/theories/Substitution/Introductions/Pi.v
@@ -280,7 +280,7 @@ Section PiTmValidity.
       exact (PiRedU tΔ Vσ).
     - intros Δ σ σ' tΔ Vσ Vσ' Vσσ'.
       pose proof (univValid (l' := zero) _ _ VFU) as VF0.
-      pose proof (irrelevanceValidity (validSnoc VΓ VF)
+      pose proof (irrelevanceTy (validSnoc VΓ VF)
                     (validSnoc (l := zero) VΓ VF0)
                     (univValid (l' := zero) _ _ VGU)) as VG0.
       unshelve econstructor ; cbn.
@@ -322,10 +322,10 @@ Section PiTmCongruence.
     pose proof (Vuσ := liftSubstS' vF Vσ).
     pose proof (Vuσσ := liftSubstSEq' vF Vσσ).
     instAllValid Vσ Vσ Vσσ; instAllValid Vuσ Vuσ Vuσσ; escape.
-    pose proof (irrelevanceValidity (validSnoc vΓ vF)
+    pose proof (irrelevanceTy (validSnoc vΓ vF)
                   (validSnoc (l := zero) vΓ vF0)
                   (univValid (l' := zero) _ _ vGU)) as vG0.
-    pose proof (irrelevanceValidity (validSnoc vΓ vF')
+    pose proof (irrelevanceTy (validSnoc vΓ vF')
                   (validSnoc (l := zero) vΓ vF'0)
                   (univValid (l' := zero) _ _ vG'U)) as vG'0.
     unshelve econstructor ; cbn.
@@ -338,7 +338,7 @@ Section PiTmCongruence.
       refine (PiEqRed2 vΓ vF0 vG0 vF'0 vG'0 _ _ tΔ Vσ).
       + exact (univEqValid vΓ (UValid vΓ) vF0 vFF').
       + pose proof (univEqValid (validSnoc vΓ vF) vU (univValid (l' := zero) _ _ vGU) vGG') as vGG'0.
-        refine (irrelevanceEq _ _ _ _ vGG'0).
+        refine (irrelevanceTyEq _ _ _ _ vGG'0).
   Qed.
 
 End PiTmCongruence.
diff --git a/theories/Substitution/Introductions/Sigma.v b/theories/Substitution/Introductions/Sigma.v
index 1b39480..b974ca1 100644
--- a/theories/Substitution/Introductions/Sigma.v
+++ b/theories/Substitution/Introductions/Sigma.v
@@ -185,7 +185,7 @@ Section SigTmValidity.
       exact (SigRedU tΔ Vσ).
     - intros Δ σ σ' tΔ Vσ Vσ' Vσσ'.
       pose proof (univValid (l' := zero) _ _ VFU) as VF0.
-      pose proof (irrelevanceValidity (validSnoc VΓ VF)
+      pose proof (irrelevanceTy (validSnoc VΓ VF)
                     (validSnoc (l := zero) VΓ VF0)
                     (univValid (l' := zero) _ _ VGU)) as VG0.
       unshelve econstructor ; cbn.
@@ -227,10 +227,10 @@ Section SigTmCongruence.
     pose proof (Vuσ := liftSubstS' VF Vσ).
     pose proof (Vuσσ := liftSubstSEq' VF Vσσ).
     instAllValid Vσ Vσ Vσσ; instAllValid Vuσ Vuσ Vuσσ; escape.
-    pose proof (irrelevanceValidity (validSnoc VΓ VF)
+    pose proof (irrelevanceTy (validSnoc VΓ VF)
                   (validSnoc (l := zero) VΓ VF0)
                   (univValid (l' := zero) _ _ VGU)) as VG0.
-    pose proof (irrelevanceValidity (validSnoc VΓ VF')
+    pose proof (irrelevanceTy (validSnoc VΓ VF')
                   (validSnoc (l := zero) VΓ VF'0)
                   (univValid (l' := zero) _ _ VG'U)) as VG'0.
     unshelve econstructor ; cbn.
@@ -243,7 +243,7 @@ Section SigTmCongruence.
       refine (SigCongRed VΓ VF0 VG0 VF'0 VG'0 _ _ tΔ Vσ).
       + exact (univEqValid VΓ (UValid VΓ) VF0 VFF').
       + pose proof (univEqValid (validSnoc VΓ VF) VU (univValid (l' := zero) _ _ VGU) VGG') as VGG'0.
-        refine (irrelevanceEq _ _ _ _ VGG'0).
+        refine (irrelevanceTyEq _ _ _ _ VGG'0).
   Qed.
 
 End SigTmCongruence.
diff --git a/theories/Substitution/Introductions/SimpleArr.v b/theories/Substitution/Introductions/SimpleArr.v
index fc39971..8240dee 100644
--- a/theories/Substitution/Introductions/SimpleArr.v
+++ b/theories/Substitution/Introductions/SimpleArr.v
@@ -30,14 +30,14 @@ Section SimpleArrValidity.
     (VeqG : [Γ ||-v< l > G ≅ G' | VΓ | VG]) :
     [Γ ||-v<l> arr F G ≅ arr F' G' | VΓ | simpleArrValid _ VF VG].
   Proof.
-    eapply irrelevanceEq.
+    eapply irrelevanceTyEq.
     unshelve eapply PiCong; tea.
     + replace G⟨↑⟩ with G⟨@wk1 Γ F⟩ by now bsimpl.
       now eapply wk1ValidTy.
     + replace G'⟨↑⟩ with G'⟨@wk1 Γ F'⟩ by now bsimpl.
       now eapply wk1ValidTy.
     + replace G'⟨↑⟩ with G'⟨@wk1 Γ F⟩ by now bsimpl.
-      eapply irrelevanceEq'.
+      eapply irrelevanceTyEq'.
       2: now eapply wk1ValidTyEq.
       now bsimpl.
     Unshelve. 2: tea.
diff --git a/theories/Substitution/Irrelevance.v b/theories/Substitution/Irrelevance.v
index a78a4cf..5515837 100644
--- a/theories/Substitution/Irrelevance.v
+++ b/theories/Substitution/Irrelevance.v
@@ -92,7 +92,7 @@ Proof.
     now eapply validTail.
 Qed.
 
-Lemma irrelevanceValidity {Γ} : forall (VΓ VΓ' : [||-v Γ]) {l A},
+Lemma irrelevanceTy {Γ} : forall (VΓ VΓ' : [||-v Γ]) {l A},
   [Γ ||-v<l> A | VΓ] -> [Γ ||-v<l> A | VΓ'].
 Proof.
   intros VΓ VΓ' l A [VA VAext]; unshelve econstructor; intros.
@@ -100,10 +100,10 @@ Proof.
   - eapply VAext; [eapply irrelevanceSubst| eapply irrelevanceSubstEq]; eassumption.
 Qed.
 
-Lemma irrelevanceValidity' {Γ Γ' A A' l} (VΓ : [||-v Γ]) (VΓ' : [||-v Γ']) (VA : [Γ ||-v<l> A | VΓ]) : 
+Lemma irrelevanceTy' {Γ Γ' A A' l} (VΓ : [||-v Γ]) (VΓ' : [||-v Γ']) (VA : [Γ ||-v<l> A | VΓ]) : 
   A = A' -> Γ = Γ' -> [Γ' ||-v<l> A' | VΓ'].
 Proof.
-  intros eqA eqΓ; subst; now eapply irrelevanceValidity.
+  intros eqA eqΓ; subst; now eapply irrelevanceTy.
 Qed.
 
 Lemma irrelevanceLift {l A F G Γ} (VΓ : [||-v Γ])
@@ -126,7 +126,7 @@ Proof.
       eapply LRTyEqSym; unshelve eapply VFeqG; eassumption.
 Qed.
 
-Lemma irrelevanceEq {Γ l A B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v<l> A | VΓ]) (VA' : [Γ||-v<l> A | VΓ']) :
+Lemma irrelevanceTyEq {Γ l A B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v<l> A | VΓ]) (VA' : [Γ||-v<l> A | VΓ']) :
   [Γ ||-v< l > A ≅ B | VΓ | VA] -> [Γ ||-v< l > A ≅ B | VΓ' | VA'].
 Proof.
   intros [h]; constructor; intros.
@@ -135,13 +135,13 @@ Proof.
   eapply irrelevanceSubst; eassumption.
 Qed.
 
-Lemma irrelevanceEq' {Γ l A A' B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v<l> A | VΓ]) (VA' : [Γ||-v<l> A' | VΓ']) : A = A' ->
+Lemma irrelevanceTyEq' {Γ l A A' B} (VΓ VΓ' : [||-v Γ]) (VA : [Γ ||-v<l> A | VΓ]) (VA' : [Γ||-v<l> A' | VΓ']) : A = A' ->
   [Γ ||-v< l > A ≅ B | VΓ | VA] -> [Γ ||-v< l > A' ≅ B | VΓ' | VA'].
 Proof.
-  intros ->; now eapply irrelevanceEq.
+  intros ->; now eapply irrelevanceTyEq.
 Qed.
 
-Lemma symValidEq {Γ l A B} {VΓ : [||-v Γ]} {VA : [Γ ||-v<l> A | VΓ]} (VB : [Γ ||-v<l> B | VΓ]) :
+Lemma symValidTyEq {Γ l A B} {VΓ : [||-v Γ]} {VA : [Γ ||-v<l> A | VΓ]} (VB : [Γ ||-v<l> B | VΓ]) :
   [Γ ||-v<l> A ≅ B | VΓ | VA] -> [Γ ||-v<l> B ≅ A | VΓ | VB].
 Proof.
   intros; constructor; intros.
@@ -149,7 +149,7 @@ Proof.
   Unshelve. all: tea.
 Qed.
 
-Lemma transValidEq {Γ l A B C} {VΓ : [||-v Γ]}
+Lemma transValidTyEq {Γ l A B C} {VΓ : [||-v Γ]}
   {VA : [Γ ||-v<l> A | VΓ]} {VB : [Γ ||-v<l> B | VΓ]} :
   [Γ ||-v<l> A ≅ B | VΓ | VA] -> [Γ ||-v<l> B ≅ C | VΓ | VB] -> [Γ ||-v<l> A ≅ C | VΓ | VA].
 Proof.
@@ -280,8 +280,8 @@ Ltac irrValid :=
   | [_ : _ |- [||-v _]] => idtac
   | [_ : _ |- [ _ ||-v _ : _ | _ | _]] => eapply irrelevanceSubst
   | [_ : _ |- [ _ ||-v _ ≅ _ : _ | _ | _ | _]] => eapply irrelevanceSubstEq
-  | [_ : _ |- [_ ||-v<_> _ | _]] => eapply irrelevanceValidity
-  | [_ : _ |- [_ ||-v<_> _ ≅ _ | _ | _]] => eapply irrelevanceEq
+  | [_ : _ |- [_ ||-v<_> _ | _]] => eapply irrelevanceTy
+  | [_ : _ |- [_ ||-v<_> _ ≅ _ | _ | _]] => eapply irrelevanceTyEq
   | [_ : _ |- [_ ||-v<_> _ : _ | _ | _]] => eapply irrelevanceTm
   | [_ : _ |- [_ ||-v<_> _ ≅ _ : _ | _ | _]] => eapply irrelevanceTmEq
   end; eassumption.
\ No newline at end of file
diff --git a/theories/Substitution/Properties.v b/theories/Substitution/Properties.v
index 2cefbf7..89ff10a 100644
--- a/theories/Substitution/Properties.v
+++ b/theories/Substitution/Properties.v
@@ -417,7 +417,7 @@ Proof.
     eapply (validHead v).
 Qed.
 
-Lemma wkValid {l Γ Δ A} (ρ : Δ ≤ Γ)
+Lemma wkValidTy {l Γ Δ A} (ρ : Δ ≤ Γ)
   (VΓ : [||-v Γ])
   (VΔ : [||-v Δ])
   (VA : [Γ ||-v<l> A | VΓ]) :
@@ -435,12 +435,12 @@ Proof.
     Unshelve. 2,3: tea.
 Qed.
 
-Lemma wkTmValid {l Γ Δ A t} (ρ : Δ ≤ Γ)
+Lemma wkValidTm {l Γ Δ A t} (ρ : Δ ≤ Γ)
   (VΓ : [||-v Γ])
   (VΔ : [||-v Δ])
   (VA : [Γ ||-v<l> A | VΓ])
   (Vt : [Γ ||-v<l> t : A | VΓ | VA]) :
-  [Δ ||-v<l> t⟨ρ⟩ : A⟨ρ⟩ | VΔ | wkValid ρ VΓ VΔ VA].
+  [Δ ||-v<l> t⟨ρ⟩ : A⟨ρ⟩ | VΔ | wkValidTy ρ VΓ VΔ VA].
 Proof.
   assert (hA : forall σ, A⟨ρ⟩[σ] = A[ρ >> σ]) by (intros; now asimpl).
   assert (ht : forall σ, t⟨ρ⟩[σ] = t[ρ >> σ]) by (intros; now asimpl).
@@ -456,12 +456,12 @@ Proof.
     now eapply substS_wk.
 Qed.
 
-Lemma wkEqValid {l Γ Δ A B} (ρ : Δ ≤ Γ)
+Lemma wkValidTyEq {l Γ Δ A B} (ρ : Δ ≤ Γ)
   (VΓ : [||-v Γ])
   (VΔ : [||-v Δ])
   (VA : [Γ ||-v<l> A | VΓ])
   (VAB : [Γ ||-v<l> A ≅ B | VΓ | VA]) :
-  [Δ ||-v<l> A⟨ρ⟩ ≅ B⟨ρ⟩ | VΔ | wkValid ρ VΓ VΔ VA].
+  [Δ ||-v<l> A⟨ρ⟩ ≅ B⟨ρ⟩ | VΔ | wkValidTy ρ VΓ VΔ VA].
 Proof.
   assert (h : forall A σ, A⟨ρ⟩[σ] = A[ ρ >> σ]) by (intros; now asimpl).
   unshelve econstructor; intros; irrelevance0; rewrite h; [reflexivity|].
diff --git a/theories/Substitution/SingleSubst.v b/theories/Substitution/SingleSubst.v
index 858f6fb..69cda66 100644
--- a/theories/Substitution/SingleSubst.v
+++ b/theories/Substitution/SingleSubst.v
@@ -194,7 +194,7 @@ Lemma substLiftSEq' {Γ F G G' t t' l} (VΓ : [||-v Γ])
   (Vtt' : [Γ,, F ||-v<l> t ≅ t' : F⟨@wk1 Γ F⟩ | VΓF | VF']) :
   [Γ ,, F ||-v<l> G[t]⇑ ≅ G'[t']⇑ | VΓF | substLiftS _ VF VG Vt].
 Proof.
-  eapply transValidEq.
+  eapply transValidTyEq.
   1: eapply substLiftSEq; [| exact VGeq]; tea.
   constructor; intros; irrelevance0; rewrite liftSubstComm ; [reflexivity|].
   instValid Vσ.