Support terminal exact contradiction

2 files changed, 15 insertions, 0 deletions

diff --git a/test/phase5/exact-contradiction-goal.tex b/test/phase5/exact-contradiction-goal.tex
new file mode 100644
index 0000000..007683f
--- /dev/null
+++ b/test/phase5/exact-contradiction-goal.tex
@@ -0,0 +1,7 @@
+\begin{proposition}\label{phase5_invalid_contradiction}
+    For all $A$ we have $A = A$.
+\end{proposition}
+\begin{proof}
+    Fix $A$.
+    Contradiction.
+\end{proof}
diff --git a/test/phase5/exact-contradiction.tex b/test/phase5/exact-contradiction.tex
new file mode 100644
index 0000000..3f2378b
--- /dev/null
+++ b/test/phase5/exact-contradiction.tex
@@ -0,0 +1,8 @@
+\begin{proposition}\label{phase5_contradiction}
+    Suppose $A \neq A$.
+    Then $A \neq A$.
+\end{proposition}
+\begin{proof}
+    Assume $A = A$.
+    Contradiction.
+\end{proof}