diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Term.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Term.ml
index 63a65a35a73..7066a54054f 100644
--- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Term.ml
+++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Term.ml
@@ -1490,13 +1490,13 @@ let (injective_constructor :
                    match uu___2 with
                    | { field_name = name1; field_sort = s;
                        field_projectible = projectible;_} ->
-                       let cproj_app = mkApp (name1, [capp]) norng in
-                       let proj_name =
-                         DeclFun
-                           (name1, [sort1], s,
-                             (FStar_Pervasives_Native.Some "Projector")) in
                        if projectible
                        then
+                         let cproj_app = mkApp (name1, [capp]) norng in
+                         let proj_name =
+                           DeclFun
+                             (name1, [sort1], s,
+                               (FStar_Pervasives_Native.Some "Projector")) in
                          let a =
                            let uu___3 =
                              let uu___4 =
@@ -1520,7 +1520,7 @@ let (injective_constructor :
                              assumption_fact_ids = []
                            } in
                          [proj_name; Assume a]
-                       else [proj_name]) fields in
+                       else []) fields in
           FStar_Compiler_List.flatten uu___1
 let (discriminator_name : constructor_t -> Prims.string) =
   fun constr -> Prims.strcat "is-" constr.constr_name
diff --git a/src/smtencoding/FStar.SMTEncoding.Term.fst b/src/smtencoding/FStar.SMTEncoding.Term.fst
index 93ceba286ee..07857606bf2 100644
--- a/src/smtencoding/FStar.SMTEncoding.Term.fst
+++ b/src/smtencoding/FStar.SMTEncoding.Term.fst
@@ -583,17 +583,18 @@ let injective_constructor
     let capp = mkApp(name, bvars) norng in
     fields
     |> List.mapi (fun i {field_projectible=projectible; field_name=name; field_sort=s} ->
-            let cproj_app = mkApp(name, [capp]) norng in
-            let proj_name = DeclFun(name, [sort], s, Some "Projector") in
             if projectible
-            then let a = {
+            then
+              let cproj_app = mkApp(name, [capp]) norng in
+              let proj_name = DeclFun(name, [sort], s, Some "Projector") in
+              let a = {
                     assumption_name = escape ("projection_inverse_"^name);
                     assumption_caption = Some "Projection inverse";
                     assumption_term = mkForall rng ([[capp]], bvar_names, mkEq(cproj_app, bvar i s norng) norng);
                     assumption_fact_ids = []
                  } in
-                 [proj_name; Assume a]
-            else [proj_name])
+              [proj_name; Assume a]
+            else [])
     |> List.flatten
 
 let discriminator_name constr = "is-"^constr.constr_name
diff --git a/tests/bug-reports/BugBoxInjectivity.fst b/tests/bug-reports/BugBoxInjectivity.fst
index c488bfbed1d..db7f646c1fe 100644
--- a/tests/bug-reports/BugBoxInjectivity.fst
+++ b/tests/bug-reports/BugBoxInjectivity.fst
@@ -12,85 +12,47 @@ let bad (h0:ceq true true) (h1:ceq false false) : Lemma (true == false) =
   let Refl = h1 in
   ()
 
-// open FStar.Functions
-// module CC = FStar.Cardinality.Universes
+open FStar.Functions
+module CC = FStar.Cardinality.Universes
 
-// type t (a:Type u#1) : Type u#0 =
-//   | Mk : t a
+type t (a:Type u#1) : Type u#0 =
+  | Mk : t a
 
-// let inj_t (#a:Type u#1) (x:t a)
-// : Lemma (x == Mk #a)
-// = let Mk #_ = x in ()
+let inj_t (#a:Type u#1) (x:t a)
+: Lemma (x == Mk #a)
+= let Mk #_ = x in ()
 
-// [@@expect_failure]
-// let t_injective : squash (is_inj t) = 
-//   introduce forall f0 f1.
-//       t f0 == t f1 ==> f0 == f1
-//   with introduce _ ==> _
-//   with _ . (
-//     inj_t #f0 Mk;
-//     inj_t #f1 (coerce_eq () (Mk #f0)) 
-//   )
+[@@expect_failure]
+let t_injective : squash (is_inj t) = 
+  introduce forall f0 f1.
+      t f0 == t f1 ==> f0 == f1
+  with introduce _ ==> _
+  with _ . (
+    inj_t #f0 Mk;
+    inj_t #f1 (coerce_eq () (Mk #f0)) 
+  )
 
 
-// #restart-solver
-// #push-options "--log_queries --query_stats --debug BugBoxInjectivity --debug_level SMTEncoding"
-// module CC = FStar.Cardinality.Universes
-// noeq
-// type test (a:Type u#0 -> Type u#1) : Type u#1 =
-//   | Mk : test a
-
-// let const (f:Type u#1) : Type u#0 -> Type u#1 = fun _ -> f
-// let itest (f:Type u#1) : Type u#1 = test (const f)
-// let itest_inhabited (f:Type u#1) : itest f = Mk 
-// let const_inversion (f0 f1:Type u#1)
-// : Lemma 
-//   (requires const f0 == const f1)
-//   (ensures f0 == f1)
-// = let _f0 = const f0 int in
-//   let _f1 = const f1 int in
-//   assert (_f0 == _f1);
-//   ()
-// let itest_injective (f0 f1:Type u#1) 
-// : Lemma
-//   (ensures itest f0 == itest f1 ==> const f0 == const f1)
-// = let x : test (const f0) = itest_inhabited f0 in
-//   let Mk #_ = x in
-//   ()
-// open FStar.Functions
-// let itest_injective' : squash (is_inj itest) = 
-//   introduce forall f0 f1.
-//       itest f0 == itest f1 ==> f0 == f1
-//   with introduce _ ==> _
-//   with _ . (
-//     itest_injective f0 f1;
-//     const_inversion f0 f1
-//   )
-// [@@expect_failure [189]] //itest is not in the right universe to use this lemma
-// let fals : squash False =
-//   CC.no_inj_universes_suc itest
-
-
-// #push-options "--ext 'compat:injectivity'"
-// noeq
-// type test2 (a:Type u#2) : Type u#1 =
-//   | Mk2 : test2 a
-// #pop-options
-
-// let test2_inhabited (f:Type u#2) : test2 f = Mk2
-// let test2_injective (f0 f1:Type u#2) 
-// : Lemma
-//   (ensures test2 f0 == test2 f1 ==> f0 == f1)
-// = let x : test2 f0 = test2_inhabited f0 in
-//   let Mk2 #_ = x in
-//   ()
-// open FStar.Functions
-// let itest2_injective' : squash (is_inj test2) = 
-//   introduce forall f0 f1.
-//       test2 f0 == test2 f1 ==> f0 == f1
-//   with introduce _ ==> _
-//   with _ . (
-//     test2_injective f0 f1
-//   )
-// let fals () : squash False =
-//   CC.no_inj_universes_suc test2
\ No newline at end of file
+#push-options "--ext 'compat:injectivity'"
+noeq
+type test2 (a:Type u#2) : Type u#1 =
+  | Mk2 : test2 a
+#pop-options
+
+let test2_inhabited (f:Type u#2) : test2 f = Mk2
+let test2_injective (f0 f1:Type u#2) 
+: Lemma
+  (ensures test2 f0 == test2 f1 ==> f0 == f1)
+= let x : test2 f0 = test2_inhabited f0 in
+  let Mk2 #_ = x in
+  ()
+open FStar.Functions
+let itest2_injective' : squash (is_inj test2) = 
+  introduce forall f0 f1.
+      test2 f0 == test2 f1 ==> f0 == f1
+  with introduce _ ==> _
+  with _ . (
+    test2_injective f0 f1
+  )
+let fals () : squash False =
+  CC.no_inj_universes_suc test2
\ No newline at end of file