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

inductive one: Type| o1inductive two: Type| t1 | t2theorem one_neq_two: one ≠ two :=have h1 : ∀ x y : one, x = y := by  intros x y; cases x; cases y; rflhave h2 : two.t1 ≠ two.t2 :=  by intro h; cases hλ h => byrw [h] at h1exact h2 (h1 two.t1 two.t2)