have : (step 1 : ℤ) ≃ (0 : ℤ) := calc
  (step 1 : ℤ)           ≃ _ := AA.subst₁ (AA.subst₁ (Rel.symm AA.identR))
  (step (1 + 0) : ℤ)     ≃ _ := AA.subst₁ AA.scompatR
  ((1 + step 0 : ℕ) : ℤ) ≃ _ := AA.subst₁ (AA.substR ‹step 0 ≃ 1›)
  ((1 + 1 : ℕ) : ℤ)      ≃ _ := AA.compat₂
  (1 : ℤ) + (1 : ℤ)      ≃ _ := AA.substR (Rel.symm ‹-1 ≃ (1 : ℤ)›)
  1 + -1                 ≃ _ := AA.inverseR
  0                      ≃ _ := Rel.refl
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this : step 0 ≃ 1
⊢ False
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
this✝ : step 0 ≃ 1
this : coe (step 1) ≃ 0
⊢ False