From 22e4eba441c9a2205798031b533b4e5d0e2b3054 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 9 Jul 2025 00:22:54 +0200
Subject: `fld_cons` faster proof (down from 12s)

---
 library/relation.tex | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/library/relation.tex b/library/relation.tex
index c653e29..a93a623 100644
--- a/library/relation.tex
+++ b/library/relation.tex
@@ -419,12 +419,21 @@
     $\fld{\emptyset} = \emptyset$.
 \end{proposition}
 
-% TODO SLOW
 \begin{proposition}\label{fld_cons}
     $\fld{(\cons{(a,b)}{R})} = \cons{a}{\cons{b}{\fld{R}}}$.
 \end{proposition}
 \begin{proof}
-    Follows by set extensionality.
+    \begin{align*}
+        \fld{(\cons{(a,b)}{R})}
+        &= \dom{(\cons{(a,b)}{R})}\union\ran{(\cons{(a,b)}{R})}
+            \explanation{by \cref{fld}}\\
+        &= \cons{a}{\dom{R}}\union\cons{b}{\ran{R}}
+            \explanation{by \cref{dom_cons,ran_cons}}\\
+        &= \cons{a}{\cons{b}{\dom{R}\union\ran{R}}}
+            \explanation{by \cref{union_cons,union_comm}}\\
+        &= \cons{a}{\cons{b}{\fld{R}}}
+          \explanation{by \cref{fld}}
+    \end{align*}
 \end{proof}
 
 \begin{proposition}\label{fld_union}
-- 
cgit v1.2.3