From 33fcae822e17838b11e88998492a7ec254b83548 Mon Sep 17 00:00:00 2001
From: 0xd34df00d <0xd34df00d@gmail.com>
Date: Fri, 1 Jan 2021 01:08:17 -0600
Subject: [PATCH] =?UTF-8?q?Prove=20=CE=B2=20on=20=E2=87=92=20implies=20?=
 =?UTF-8?q?=CE=B2=20on=20domain?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 agda/Surface/Operational/BetaEquivalence.agda | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/agda/Surface/Operational/BetaEquivalence.agda b/agda/Surface/Operational/BetaEquivalence.agda
index c9679b7d..3e468cc9 100644
--- a/agda/Surface/Operational/BetaEquivalence.agda
+++ b/agda/Surface/Operational/BetaEquivalence.agda
@@ -127,3 +127,11 @@ prove-via-≡rβ' f = ≡rβ'-to-≡rβ ∘ f ∘ ≡rβ-to-≡rβ'
            → (⊍ cons₁) ≡rβ (⊍ cons₂)
            → lookup cons₁ idx ≡rβ lookup cons₂ idx
 ≡rβ-lookup idx = prove-via-≡rβ' (≡rβ'-lookup idx _ _)
+
+≡rβ'-⇒-dom : (τ₁' ⇒ τ₂') ≡rβ' (τ₁ ⇒ τ₂)
+           → τ₁' ≡rβ' τ₁
+≡rβ'-⇒-dom (≡rβ'-Subst ε ε' (τ₀₁ ⇒ τ₀₂) ε↝ε' refl refl) = ≡rβ'-Subst ε ε' τ₀₁ ε↝ε' refl refl
+
+≡rβ-⇒-dom : (τ₁' ⇒ τ₂') ≡rβ (τ₁ ⇒ τ₂)
+          → τ₁' ≡rβ τ₁
+≡rβ-⇒-dom = prove-via-≡rβ' ≡rβ'-⇒-dom