## § 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)
```