From 67561abf1af3c6b7d2ef81e58266289bfdc54b6e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 18 Nov 2024 11:43:50 +1100
Subject: [PATCH 1/2] feat: add a test replacing an axiom

---
 test.sh | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/test.sh b/test.sh
index 46a2d95..e42a0d6 100755
--- a/test.sh
+++ b/test.sh
@@ -32,6 +32,14 @@ but it is expected to have type
 check_command "lake -q exe lean4checker Lean4CheckerTests.AddFalseConstructor" "lean4checker found a problem in Lean4CheckerTests.AddFalseConstructor
 uncaught exception: No such constructor False.intro"
 
+check_command "lake -q exe lean4checker Lean4CheckerTests.ReplaceAxiom" "lean4checker found a problem in Lean4CheckerTests.ReplaceAxiom
+uncaught exception: application type mismatch
+  False.elim @propext
+argument has type
+  ∀ {a b : Prop}, (a ↔ b) → a = b
+but function has type
+  False → ∀ (x y z n : Nat), 0 < x → 0 < y → 0 < z → 2 < n → x ^ n + y ^ n ≠ z ^ n"
+
 check_command "lake -q exe lean4checker --fresh Lean4CheckerTests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"
 
 # The 'ReduceBool' test writes to a temporary file.

From df48ccccab1711e5ba4acf5de9f58837f08ad579 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 18 Nov 2024 11:43:54 +1100
Subject: [PATCH 2/2] feat: add a test replacing an axiom

---
 Lean4CheckerTests/ReplaceAxiom.lean | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 Lean4CheckerTests/ReplaceAxiom.lean

diff --git a/Lean4CheckerTests/ReplaceAxiom.lean b/Lean4CheckerTests/ReplaceAxiom.lean
new file mode 100644
index 0000000..2871098
--- /dev/null
+++ b/Lean4CheckerTests/ReplaceAxiom.lean
@@ -0,0 +1,27 @@
+import Lean4CheckerTests.OpenPrivate
+
+/- Redefine `propext : False`. -/
+open Lean Elab Meta in
+open private Environment.mk from Lean.Environment in
+#eval modifyEnv (m := MetaM) fun env =>
+  let consts :=
+    { env.constants with
+        map₁ := env.constants.map₁.insert ``propext (.axiomInfo {
+          name := ``propext
+          type := .const ``False []
+          levelParams := []
+          isUnsafe := false
+        })
+    }
+  Environment.mk env.const2ModIdx consts env.extensions env.extraConstNames env.header
+
+theorem efsq : ∀ (x y z n : Nat),
+    0 < x → 0 < y → 0 < z → 2 < n →
+    x^n + y^n ≠ z^n := by
+  exfalso
+  exact propext
+
+/-- info: 'efsq' depends on axioms: [propext] -/
+#guard_msgs in
+-- 'efsq' depends on axioms: [propext]
+#print axioms efsq