diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 384d0a5..cb80128 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -569,3 +569,15 @@ record Graph : Set where
                 n₂₃→n₁₂,₃ = n₂→n'×n₃→n'⇒n₂₃→n' n₁₂,₃ (n₂→n₁₂ ++ n₁₂→n₁₂,₃ , n₃→n₁₂,₃)
                 n₁,₂₃→n₁₂,₃ = n₁→n'×n₂₃→n'⇒n₁,₂₃→n' n₁₂,₃ (n₁→n₁₂ ++ n₁₂→n₁₂,₃ , n₂₃→n₁₂,₃)
             in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃
+
+        ⊔-⊓-absorb : ∀ n₁ n₂ → n₁ ⊔ (n₁ ⊓ n₂) ≡ n₁
+        ⊔-⊓-absorb n₁ n₂
+            with (n₁₂ , ((n₁→n₁₂ , n₂→n₁₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
+            with (n₁,₁₂ , ((n₁,₁₂→n₁ , n₁,₁₂→n₁₂) , n'→n₁×n'→n₁₂⇒n'→n₁,₁₂)) ← total-⊔ n₁ n₁₂
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁,₁₂→n₁ (n'→n₁×n'→n₁₂⇒n'→n₁,₁₂ n₁ (done , n₁→n₁₂))
+
+        ⊓-⊔-absorb : ∀ n₁ n₂ → n₁ ⊓ (n₁ ⊔ n₂) ≡ n₁
+        ⊓-⊔-absorb n₁ n₂
+            with (n₁₂ , ((n₁₂→n₁ , n₁₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
+            with (n₁,₁₂ , ((n₁→n₁,₁₂ , n₁₂→n₁,₁₂) , n₁→n'×n₁₂→n'⇒n₁,₁₂→n')) ← total-⊓ n₁ n₁₂
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₁₂→n'⇒n₁,₁₂→n' n₁ (done , n₁₂→n₁)) n₁→n₁,₁₂