1 files changed, 8 insertions, 0 deletions
diff --git a/test/phase5/exact-relational-replacement-local-failure.tex b/test/phase5/exact-relational-replacement-local-failure.tex
new file mode 100644
index 0000000..6a051cd
--- /dev/null
+++ b/test/phase5/exact-relational-replacement-local-failure.tex
@@ -0,0 +1,8 @@
+\begin{proposition}\label{phase5_relational_local_failure}
+    For every set $A$ we have $A = A$.
+\end{proposition}
+\begin{proof}
+    Fix $A$.
+    Let $B = \{ y \mid \exists x\in A. y = y \}$.
+    Follows.
+\end{proof}