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