Prove β on ⇒ implies β on domain

0xd34df00d · Jan 1, 2021 · 33fcae8 · 33fcae8
1 parent 335692e
commit 33fcae8
Showing 1 changed file with 8 additions and 0 deletions.
diff --git 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