From c9ed022c35cdc13bba4cc2b624295ea80b38d0a7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 25 Jun 2024 00:02:04 +0200
Subject: Improvement for the ATP proof time

---
 library/relation.tex | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'library/relation.tex')

diff --git a/library/relation.tex b/library/relation.tex
index b5aebcd..4c4065f 100644
--- a/library/relation.tex
+++ b/library/relation.tex
@@ -422,6 +422,9 @@
 \begin{proposition}\label{fld_cons}
     $\fld{(\cons{(a,b)}{R})} = \cons{a}{\cons{b}{\fld{R}}}$.
 \end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
 
 \begin{proposition}\label{fld_union}
     $\fld{(A\union B)} = \fld{A}\union\fld{B}$.
-- 
cgit v1.2.3