have : Natural.step (0 : ℕ) ≃ 0 :=
  Rel.trans (Rel.symm Natural.literal_step) ‹(1 : ℕ) ≃ 0›
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝ : coe 1 ≃ coe 0
this : 1 ≃ 0
⊢ False
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝¹ : coe 1 ≃ coe 0
this✝ : 1 ≃ 0
this : Natural.step 0 ≃ 0
⊢ False