From b17bbaf5d5c208fc5a1513acb9b6f96d734bba1c Mon Sep 17 00:00:00 2001
From: KonjacSource <1435771606@qq.com>
Date: Mon, 9 Sep 2024 16:11:47 +0800
Subject: [PATCH] unmatchable, axiom

---
 README-zh.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/README-zh.md b/README-zh.md
index 200a3e0..0fc35d0 100644
--- a/README-zh.md
+++ b/README-zh.md
@@ -202,7 +202,6 @@ higher inductive S1 : U where
     | i1 = base
 ```
 
-
 ### 定理证明?
 
 ShiTT 不是一个 PA, 所以这里直接使用了 Type in Type, 并且将来可能考虑不添加终止检查.