§ Any model of lean must have all inductives

• Or, lean knows about the sizes of types.
• See that the below proof script shows that

inductive one: Type
| o1

inductive two: Type
| t1 | t2

theorem one_neq_two: one ≠ two :=
have h1 : ∀ x y : one, x = y := by
  intros x y; cases x; cases y; rfl
have h2 : two.t1 ≠ two.t2 :=
  by intro h; cases h
λ h => by
rw [h] at h1
exact h2 (h1 two.t1 two.t2)