From b6e357787fe43f7dae54d2c9ed85324f725413fd Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 13 Apr 2024 12:25:59 -0700
Subject: [PATCH] Add proof about 'both' and pairing

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Language.agda b/Language.agda
index e73cbf2..7cdf8a0 100644
--- a/Language.agda
+++ b/Language.agda
@@ -278,7 +278,11 @@ module Graphs where
                  {P-Mono : MonotonicPredicate P}
                  {m₁ : MonotonicGraphFunction T₁} {m₂ : MonotonicGraphFunction T₂} →
                  always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂)
-    ⟨⊗⟩-reason = {!!}
+    ⟨⊗⟩-reason {P-Mono = P-Mono} {m₁ = m₁} {m₂ = m₂} aP aQ g
+        with p ← aP g
+        with (g' , (t₁ , g⊆g')) ← m₁ g
+        with q ← aQ g'
+        with (g'' , (t₂ , g'⊆g'')) ← m₂ g' = (P-Mono _ _ _ g'⊆g'' p , q)
 
     module Construction where
         pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index