yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix soundness

Browse source
This commit is contained in:
Yiyun Liu 2025-04-18 15:46:07 -04:00
parent d9282fb815
commit 43daff1b27
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
theories/soundness.v
View file

@ -7,7 +7,7 @@ Theorem fundamental_theorem :
(forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A) /\ (forall Γ a A, Γ ⊢ a ∈ A -> Γ ⊨ a ∈ A) /\
(forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\ (forall Γ a b A, Γ ⊢ a ≡ b ∈ A -> Γ ⊨ a ≡ b ∈ A) /\
(forall Γ a b, Γ ⊢ a ≲ b -> Γ ⊨ a ≲ b). (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. Unshelve. all : exact 0.
Qed. Qed.