minimal declarations to get noConfusion

test.lean

prelude
set_option autoImplicit true

universe u v w

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive PUnit : Sort u where
  | unit : PUnit

inductive True : Prop where
  | intro : True

inductive Eq : α → α → Prop where
  | refl (a : α) : Eq a a

abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b :=
  h.rec m

inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
  | refl (a : α) : HEq a a

structure Prod (α : Type u) (β : Type v) where
  fst : α
  snd : β

structure PProd (α : Sort u) (β : Sort v) where
  fst : α
  snd : β

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

#check Nat.noConfusion