diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v
index 16b08798..37d49f20 100644
--- a/theories/Core/Completeness/FundamentalTheorem.v
+++ b/theories/Core/Completeness/FundamentalTheorem.v
@@ -16,9 +16,9 @@ Section completeness_fundamental.
   Theorem completeness_fundamental :
     (forall Γ, {{ ⊢ Γ }} -> {{ ⊨ Γ }}) /\
       (forall Γ Γ', {{ ⊢ Γ ⊆ Γ' }} -> {{ SubE Γ <: Γ' }}) /\
-      (forall Γ M A, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\
+      (forall Γ A M, {{ Γ ⊢ M : A }} -> {{ Γ ⊨ M : A }}) /\
       (forall Γ A M M', {{ Γ ⊢ M ≈ M' : A }} -> {{ Γ ⊨ M ≈ M' : A }}) /\
-      (forall Γ σ Δ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\
+      (forall Γ Δ σ, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊨s σ : Δ }}) /\
       (forall Γ Δ σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ Γ ⊨s σ ≈ σ' : Δ }}) /\
       (forall Γ A A', {{ Γ ⊢ A ⊆ A' }} -> {{ Γ ⊨ A ⊆ A' }}).
   Proof.
diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v
index accdac2c..24a7f678 100644
--- a/theories/Core/Soundness/Realizability.v
+++ b/theories/Core/Soundness/Realizability.v
@@ -65,9 +65,9 @@ Proof.
       * rewrite <- H4. trivial.
       * intros.
         saturate_weakening_escape.
-        assert {{ Δ ⊢ T [σ] ≈ Type @ j[σ] : Type @ i }} by mauto 3.
         rewrite <- wf_exp_eq_typ_sub; try eassumption.
-        rewrite <- H12. firstorder.
+        rewrite <- H4.
+        firstorder.
   - deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
     firstorder.
     specialize (H _ _ _ H9) as [? []].
@@ -81,8 +81,7 @@ Proof.
       progressive_invert H15.
       deepexec H20 ltac:(fun H => pose proof H).
       functional_read_rewrite_clear.
-      assert {{ Δ ⊢ T [σ] ≈ Type @ j[σ] : Type @ i }} by mauto 3.
-      rewrite H19.
+      rewrite H6.
       autorewrite with mcltt.
       trivial.
 
@@ -106,8 +105,7 @@ Proof.
     + mauto 2.
     + intros.
       saturate_weakening_escape.
-      assert {{ Δ ⊢ T [σ] ≈ ℕ[σ] : Type @ i }} by mauto 3.
-      rewrite H9.
+      rewrite H1.
       autorewrite with mcltt.
       mauto using glu_nat_readback.
 
@@ -124,6 +122,7 @@ Proof.
       progressive_invert H16.
       destruct (H9 _ _ _ H0 H12) as [].
 
+      
       transitivity {{{(Π IT OT) [σ]}}};[mauto 3 |].
       transitivity {{{Π (IT [ σ ]) (OT [q σ])}}};[mauto 3 |].
       simpl. apply wf_exp_eq_pi_cong'; [firstorder |].
diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
index 3fe37412..062a8194 100644
--- a/theories/Core/Syntactic/Corollaries.v
+++ b/theories/Core/Syntactic/Corollaries.v
@@ -26,8 +26,8 @@ Qed.
 #[export]
 Hint Resolve invert_sub_id : mcltt.
 
-Add Parametric Morphism i Γ Δ t (H : {{ Δ ⊢ t : Type@i }}) : (a_sub t)
-    with signature wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong1.
+Add Parametric Morphism i Γ Δ : a_sub
+    with signature wf_exp_eq Δ {{{ Type@i }}} ==> wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong.
 Proof.
   intros.
   gen_presups.
diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
index 26de2d49..0105b184 100644
--- a/theories/Core/Syntactic/CtxEq.v
+++ b/theories/Core/Syntactic/CtxEq.v
@@ -41,8 +41,8 @@ Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 
 Proof with mautosolve.
   intros * HΓ01.
   gen Γ2.
-  induction HΓ01 as [|Γ0 ? T0 i01 T1]; mauto.
-  inversion_clear 1 as [|? Γ2' ? i12 T2].
+  induction HΓ01 as [|Γ0 ? i01 T0 T1]; mauto.
+  inversion_clear 1 as [|? Γ2' i12 ? T2].
   clear Γ2; rename Γ2' into Γ2.
   set (i := max i01 i12).
   assert {{ Γ0 ⊢ T0 : Type@i }} by mauto using lift_exp_max_left.
diff --git a/theories/Core/Syntactic/CtxSub.v b/theories/Core/Syntactic/CtxSub.v
index f8b19157..7e0d0608 100644
--- a/theories/Core/Syntactic/CtxSub.v
+++ b/theories/Core/Syntactic/CtxSub.v
@@ -49,7 +49,7 @@ Module ctxsub_judg.
     2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.
 
     - (* ctxsub_exp_eq_helper variable case *)
-      inversion_clear HΓΔ as [|Δ0 ? C'].
+      inversion_clear HΓΔ as [|Δ0 ? ? C'].
       assert (exists D, {{ #x : D ∈ Δ0 }} /\ {{ Δ0 ⊢ D ⊆ B }}) as [D [i0 ?]] by mauto.
       destruct_conjs.
       assert {{ ⊢ Δ0, C' }} by mauto.
diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v
index 06e436d7..68554069 100644
--- a/theories/Core/Syntactic/System/Definitions.v
+++ b/theories/Core/Syntactic/System/Definitions.v
@@ -39,7 +39,7 @@ with wf_ctx_sub : ctx -> ctx -> Prop :=
      {{ ⊢ Γ , A ⊆ Δ , A' }} )
 where "⊢ Γ ⊆ Γ'" := (wf_ctx_sub Γ Γ') (in custom judg) : type_scope
 
-with wf_exp : ctx -> exp -> typ -> Prop :=
+with wf_exp : ctx -> typ -> exp -> Prop :=
 | wf_typ :
   `( {{ ⊢ Γ }} ->
      {{ Γ ⊢ Type@i : Type@(S i) }} )
@@ -84,9 +84,9 @@ with wf_exp : ctx -> exp -> typ -> Prop :=
   `( {{ Γ ⊢ M : A }} ->
      {{ Γ ⊢ A ⊆ A' }} ->
      {{ Γ ⊢ M : A' }} )
-where "Γ ⊢ M : A" := (wf_exp Γ M A) (in custom judg) : type_scope
+where "Γ ⊢ M : A" := (wf_exp Γ A M) (in custom judg) : type_scope
 
-with wf_sub : ctx -> sub -> ctx -> Prop :=
+with wf_sub : ctx -> ctx -> sub -> Prop :=
 | wf_sub_id :
   `( {{ ⊢ Γ }} ->
      {{ Γ ⊢s Id : Γ }} )
@@ -106,7 +106,7 @@ with wf_sub : ctx -> sub -> ctx -> Prop :=
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ ⊢ Δ ⊆ Δ' }} ->
      {{ Γ ⊢s σ : Δ' }} )
-where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope
+where "Γ ⊢s σ : Δ" := (wf_sub Γ Δ σ) (in custom judg) : type_scope
 
 with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
 | wf_exp_eq_typ_sub :
@@ -372,7 +372,7 @@ Qed.
 
 
 Add Parametric Morphism i Γ : (wf_exp Γ)
-    with signature eq ==> wf_exp_eq Γ {{{ Type@i }}} ==> iff as wf_exp_morph.
+    with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> iff as wf_exp_morph.
 Proof.
   intros; split; mauto.
 Qed.
@@ -390,3 +390,17 @@ Hint Rewrite -> wf_exp_eq_typ_sub wf_exp_eq_nat_sub using eassumption : mcltt.
 Hint Rewrite -> wf_sub_eq_id_compose_right wf_sub_eq_id_compose_left
                   wf_sub_eq_compose_assoc (* prefer right association *)
                   wf_sub_eq_p_extend using mauto 4 : mcltt.
+
+
+#[export]
+  Instance wf_exp_eq_per_elem Γ T : PERElem _ (wf_exp Γ T) (wf_exp_eq Γ T).
+Proof.
+  intros a Ha. mauto.
+Qed.
+
+
+#[export]
+  Instance wf_sub_eq_per_elem Γ Δ : PERElem _ (wf_sub Γ Δ) (wf_sub_eq Γ Δ).
+Proof.
+  intros a Ha. mauto.
+Qed.
diff --git a/theories/LibTactics.v b/theories/LibTactics.v
index 9a69c5e8..677a3766 100644
--- a/theories/LibTactics.v
+++ b/theories/LibTactics.v
@@ -421,3 +421,15 @@ Instance subrelation_relation_equivalence {A} : subrelation relation_equivalence
 Proof.
   intro; intuition.
 Qed.
+
+(* The following facility converts search of Proper from type class instances to the local context *)
+
+Class PERElem (A : Type) (P : A -> Prop) (R : A -> A -> Prop) :=
+  per_elem : forall a, P a -> R a a.
+
+#[export]
+  Instance PERProper (A : Type) (P : A -> Prop) (R : A -> A -> Prop) `(Ins : PERElem A P R) a (H : P a) :
+  Proper R a.
+Proof.
+  cbv. auto using per_elem.
+Qed.