intro _ h
a b : ℕ
ha : a < 4
hb : b < 4
⊢ a ≠ b → { val := a, isLt := ha } ≠ { val := b, isLt := hb }
a b : ℕ
ha : a < 4
hb : b < 4
a✝ : a ≠ b
h : { val := a, isLt := ha } = { val := b, isLt := hb }
⊢ False