From 40654301df3232dde0ec2530c6215af1aa477760 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 23 Jun 2021 14:23:16 -0300
Subject: [PATCH] adding forall equiv rule
---
spec/doc.tex | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/spec/doc.tex b/spec/doc.tex
index a2257ec..84e9119 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -2335,6 +2335,15 @@ with $1 \leq k \leq n$.
&(\currule)\\
\end{plList}
\end{plContainer}
+
+ \begin{plContainer}
+ \begin{plList}
+ \Gamma\proofsep&
+ i.& \operatorname{\forall x_1, \dots, x_n.} \varphi \leftrightarrow \operatorname{\neg\exists x_1, \dots, x_n.} \neg\varphi
+ &(\currule)\\
+ \end{plList}
+ \end{plContainer}
+
\end{proof-rule}
\begin{proof-rule}{and_simplify}{veriT}
--
GitLab