fix(library/logic): import prod and unit declarations in logic

Reason: we need them for automatically generating constructions needed
by the definitional package

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

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