diff --git a/theories/Core/Completeness/Consequences/Types.v b/theories/Core/Completeness/Consequences/Types.v
index 0af50b0..847b726 100644
--- a/theories/Core/Completeness/Consequences/Types.v
+++ b/theories/Core/Completeness/Consequences/Types.v
@@ -31,6 +31,7 @@ Inductive is_typ_constr : typ -> Prop :=
 | typ_is_typ_constr : forall i, is_typ_constr {{{ Type@i }}}
 | nat_is_typ_constr : is_typ_constr {{{ ℕ }}}
 | pi_is_typ_constr : forall A B, is_typ_constr {{{ Π A B }}}
+| eq_is_typ_constr : forall A M N, is_typ_constr {{{ Eq A M N }}}
 | var_is_typ_constr : forall x, is_typ_constr {{{ #x }}}
 .
 #[export]
diff --git a/theories/Core/Semantic/Consequences.v b/theories/Core/Semantic/Consequences.v
index 9854014..486ad0a 100644
--- a/theories/Core/Semantic/Consequences.v
+++ b/theories/Core/Semantic/Consequences.v
@@ -172,7 +172,7 @@ Lemma consistency_ne_helper : forall {i A A'} {W : ne},
     {{ ⋅, Type@i ⊢ A ⊆ A' }} ->
     ~ {{ ⋅, Type@i ⊢ W : A }}.
 Proof with (congruence + mautosolve 3).
-  intros * HA' HA'eq Heq HW. gen A'.
+ intros * HA' HA'eq Heq HW. gen A'.
   dependent induction HW; intros; mauto 3; try directed dependent destruction HA';
     try (destruct W; simpl in *; congruence).
   - destruct W; simpl in *; autoinjections.
@@ -186,6 +186,8 @@ Proof with (congruence + mautosolve 3).
       try (eapply HA'eq; mautosolve 4).
     assert {{ ⋅, Type@i ⊢ Type@i ≈ Π ^_ ^_ : Type@_ }} by mauto 3.
     assert ({{{ Π ^_ ^_ }}} = {{{ Type@i }}}) by mauto 3...
+  - destruct W; simpl in *; autoinjections.
+    eapply IHHW6; [| | | | mauto 4]...
 Qed.
 
 Theorem consistency : forall {i} M,
diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
new file mode 100644
index 0000000..ffb6363
--- /dev/null
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -0,0 +1,48 @@
+From Mctt Require Import LibTactics.
+From Mctt.Core Require Import Base.
+From Mctt.Core.Completeness Require Import FundamentalTheorem.
+From Mctt.Core.Semantic Require Import Realizability.
+From Mctt.Core.Soundness Require Import
+  ContextCases
+  LogicalRelation
+  SubstitutionCases
+  SubtypingCases
+  TermStructureCases
+  UniverseCases.
+Import Domain_Notations.
+
+
+Lemma glu_rel_eq : forall Γ A i M N,
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ M : A }} ->
+    {{ Γ ⊩ N : A }} ->
+    {{ Γ ⊩ Eq A M N : Type@i }}.
+Proof.
+Admitted.
+
+#[export]
+  Hint Resolve glu_rel_eq : mctt.
+
+Lemma glu_rel_eq_refl : forall Γ A i M,
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ M : A }} ->
+    {{ Γ ⊩ refl A M : Eq A M M }}.
+Proof.
+Admitted.
+
+#[export]
+  Hint Resolve glu_rel_eq_refl : mctt.
+
+
+Lemma glu_rel_eq_eqrec : forall Γ A i M1 M2 B j BR N,
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ M1 : A }} ->
+    {{ Γ ⊩ M2 : A }} ->
+    {{ Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 ⊩ B : Type@j }} ->
+    {{ Γ, A ⊩ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
+    {{ Γ ⊩ N : Eq A M1 M2 }} ->
+    {{ Γ ⊩ eqrec N as Eq A M1 M2 return B | refl -> BR end : B[Id,,M1,,M2,,N] }}.
+Admitted.
+
+#[export]
+  Hint Resolve glu_rel_eq_eqrec : mctt.
diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v
index bc52ac9..60e5005 100644
--- a/theories/Core/Soundness/FunctionCases.v
+++ b/theories/Core/Soundness/FunctionCases.v
@@ -54,8 +54,8 @@ Proof.
   unfold univ_glu_exp_pred' in *.
   destruct_conjs.
   rename m into a.
-  assert {{ Γ ⊨ Π A B : Type@i }} as [env_relΓ]%rel_exp_of_typ_inversion by mauto 3 using completeness_fundamental_exp.
-  assert {{ Γ, A ⊨ B : Type@i }} as [env_relΓA]%rel_exp_of_typ_inversion by mauto 3 using completeness_fundamental_exp.
+  assert {{ Γ ⊨ Π A B : Type@i }} as [env_relΓ]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
+  assert {{ Γ, A ⊨ B : Type@i }} as [env_relΓA]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
   destruct_conjs.
   match_by_head1 (per_ctx_env env_relΓA) invert_per_ctx_env.
   pose env_relΓA.
diff --git a/theories/Core/Soundness/FundamentalTheorem.v b/theories/Core/Soundness/FundamentalTheorem.v
index 593cf73..cac7a99 100644
--- a/theories/Core/Soundness/FundamentalTheorem.v
+++ b/theories/Core/Soundness/FundamentalTheorem.v
@@ -7,7 +7,8 @@ From Mctt.Core.Soundness Require Import
   SubstitutionCases
   SubtypingCases
   TermStructureCases
-  UniverseCases.
+  UniverseCases
+  EqualityCases.
 From Mctt.Core.Soundness Require Export LogicalRelation.
 Import Domain_Notations.
 
diff --git a/theories/_CoqProject b/theories/_CoqProject
index d260886..c4b20e6 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -26,7 +26,7 @@
 ./Core/Completeness/TermStructureCases.v
 ./Core/Completeness/UniverseCases.v
 ./Core/Completeness/VariableCases.v
-# ./Core/Semantic/Consequences.v
+./Core/Semantic/Consequences.v
 ./Core/Semantic/Domain.v
 ./Core/Semantic/Evaluation.v
 ./Core/Semantic/Evaluation/Definitions.v
@@ -41,22 +41,23 @@
 ./Core/Semantic/Readback/Definitions.v
 ./Core/Semantic/Readback/Lemmas.v
 ./Core/Semantic/Realizability.v
-# ./Core/Soundness.v
-# ./Core/Soundness/ContextCases.v
-# ./Core/Soundness/FunctionCases.v
-# ./Core/Soundness/FundamentalTheorem.v
+./Core/Soundness.v
+./Core/Soundness/ContextCases.v
+./Core/Soundness/FunctionCases.v
+./Core/Soundness/FundamentalTheorem.v
 ./Core/Soundness/LogicalRelation.v
 ./Core/Soundness/LogicalRelation/Core.v
 ./Core/Soundness/LogicalRelation/CoreLemmas.v
 ./Core/Soundness/LogicalRelation/CoreTactics.v
 ./Core/Soundness/LogicalRelation/Definitions.v
 ./Core/Soundness/LogicalRelation/Lemmas.v
-# ./Core/Soundness/NatCases.v
+./Core/Soundness/NatCases.v
 ./Core/Soundness/Realizability.v
-# ./Core/Soundness/SubstitutionCases.v
-# ./Core/Soundness/SubtypingCases.v
-# ./Core/Soundness/TermStructureCases.v
-# ./Core/Soundness/UniverseCases.v
+./Core/Soundness/SubstitutionCases.v
+./Core/Soundness/SubtypingCases.v
+./Core/Soundness/TermStructureCases.v
+./Core/Soundness/UniverseCases.v
+./Core/Soundness/EqualityCases.v
 ./Core/Soundness/Weakening/Definitions.v
 ./Core/Soundness/Weakening/Lemmas.v
 ./Core/Syntactic/CoreInversions.v