From 43daff1b278f9bf21cdc89f9a69faca2b0e0b82c Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Fri, 18 Apr 2025 15:46:07 -0400
Subject: [PATCH] Fix soundness

---
 theories/soundness.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/soundness.v b/theories/soundness.v
index 7f86852..877e3fb 100644
--- a/theories/soundness.v
+++ b/theories/soundness.v
@@ -7,7 +7,7 @@ Theorem fundamental_theorem :
   (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A)  /\
   (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
   (forall Γ a b, Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b).
-  apply wt_mutual; eauto with sem; [hauto l:on use:SE_Pair].
+  apply wt_mutual; eauto with sem.
   Unshelve. all : exact 0.
 Qed.