diff --git a/library/logic/default.lean b/library/logic/default.lean
index 5f21f0e1b1..a58e34a9d4 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -2,7 +2,10 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.connectives logic.eq logic.cast logic.wf
+import logic.connectives logic.eq logic.heq
+import logic.cast logic.wf
+-- We need unit and prod available for generating constructions used by definitional package
+import data.unit.decl data.prod.decl
 import logic.quantifiers logic.if
 import logic.decidable logic.inhabited logic.nonempty
 import logic.instances
diff --git a/tests/lean/run/fib_brec.lean b/tests/lean/run/fib_brec.lean
index b0766d80c2..71e53a5b4b 100644
--- a/tests/lean/run/fib_brec.lean
+++ b/tests/lean/run/fib_brec.lean
@@ -2,9 +2,6 @@ import data.nat.basic data.prod
 open prod
 
 namespace nat
-  definition below.{l} {C : nat → Type.{l}} (n : nat) :=
-  rec_on n unit.{max 1 l} (λ (n₁ : nat) (r₁ : Type.{max 1 l}), C n₁ × r₁)
-
   definition brec_on {C : nat → Type} (n : nat) (F : Π (n : nat), @below C n → C n) : C n :=
   have general : C n × @below C n, from
     rec_on n