From ac15538ea6c36d0c42b17386cc713fc485a61e3b Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Fri, 20 Sep 2024 22:47:42 +0900
Subject: [PATCH] =?UTF-8?q?=E8=A8=BC=E6=98=8E=E7=84=A1=E9=96=A2=E4=BF=82?=
 =?UTF-8?q?=E3=81=AE=E8=A1=A8=E8=A8=98=E6=8F=BA=E3=82=8C=20Fixes=20#835?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Type/Prop.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Examples/Type/Prop.lean b/Examples/Type/Prop.lean
index b15d836d..a94da004 100644
--- a/Examples/Type/Prop.lean
+++ b/Examples/Type/Prop.lean
@@ -148,7 +148,7 @@ axiom extract_bar : extract bar = -1
 
 -- このとき、以下のように矛盾が得られる
 example : False := by
-  -- 証明無関連により `foo` と `bar` は等しい
+  -- 証明無関係により `foo` と `bar` は等しい
   have irr : foo = bar := by rfl
 
   -- extract が満たすべき条件から、`1 = -1` が導けてしまう