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

Minor

Browse source
This commit is contained in:
Yiyun Liu 2025-02-06 16:31:50 -05:00
parent e7a26e6bd6
commit 82e21196c2
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
theories/logrel.v
View file

@ -539,6 +539,11 @@ Proof.
move {h}. hauto l:on use:sn_unmorphing. move {h}. hauto l:on use:sn_unmorphing.
Qed. Qed.
Lemma SemEq_SN_Join n Γ (a b A : PTm n) :
Γ ⊨ a ≡ b ∈ A ->
SN a /\ SN b /\ SN A /\ DJoin.R a b.
Proof. hauto l:on use:SemEq_SemWt, SemWt_SN. Qed.
Lemma SemWt_Univ n Γ (A : PTm n) i : Lemma SemWt_Univ n Γ (A : PTm n) i :
Γ ⊨ A ∈ PUniv i <-> Γ ⊨ A ∈ PUniv i <->
forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_PTm ρ A ⟧ i ↘ S. forall ρ, ρ_ok Γ ρ -> exists S, ⟦ subst_PTm ρ A ⟧ i ↘ S.