axiom α ≃ β → α = β と ofReduceBool は矛盾する

import Mathlib.Data.Setoid.Basic

axiom equiv_of_eq {α β : Type} (f : α ≃ β) : α = β

def Nat' := Quotient (Setoid.ker fun x : Nat ↦ x - 1)
@[simp] theorem mk_zero : (⟦0⟧ : Nat') = ⟦1⟧ := Quotient.sound rfl

def equivNat : Nat' ≃ Nat where
  toFun x := x.lift _ fun _ _ ↦ id
  invFun x := ⟦x + 1⟧
  left_inv x := x.inductionOn fun x ↦ x.recOn (by simp) (by simp)
  right_inv x := by simp

def castNat : Nat' → Nat := cast (equiv_of_eq equivNat)

theorem contradiction : False := by
  have : castNat ⟦0⟧ ≠ castNat ⟦1⟧ := by native_decide
  simpa

-- 'contradiction' depends on axioms: [equiv_of_eq, propext, Lean.ofReduceBool, Quot.sound]
#print axioms contradiction

#general > Cardinality model incompatible with Lean compiler

Reproduce the self-contained Lean snippet and inspect the axioms printed for contradiction. Then read the linked Zulip discussion about the cardinality model and compiler compatibility; the issue is complete only when the incompatibility is explained and an agreed resolution is documented.