From d8df40ab390e0f60a093f80c7aa18ed7d39aa977 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 8 Jan 2023 21:46:26 +0100
Subject: [PATCH] =?UTF-8?q?=CE=B2=E2=86=98=E2=86=99=20test?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/Tests/Equal.idr | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 2f89322..0b80cbc 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -209,6 +209,11 @@ tests = "equality & subtyping" :- [
           ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
             :@ FT "a")
           (F "a"),
+      testEq "(λ g ⇒ [g [x]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [x]  (β↘↙)" $
+        let a = FT "A"; a2a = (Arr One a a) in
+        equalE
+          ((Lam "g" (TUsed (E (BV 0 :@ FT "x"))) :# Arr One a2a a) :@ FT "f")
+          ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "x"),
       testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
         subE
           ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))