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-03-03 01:40:12 -05:00
parent b3bd75ad42
commit 896d22ac9b
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
theories/logrel.v
View file

@ -1579,7 +1579,6 @@ Proof.
Qed.
Lemma SSu_Pi Γ (A0 A1 : PTm ) B0 B1 :
⊨ Γ ->
Γ ⊨ A1 ≲ A0 ->
cons A0 Γ ⊨ B0 ≲ B1 ->
Γ ⊨ PBind PPi A0 B0 ≲ PBind PPi A1 B1.
@ -1602,12 +1601,11 @@ Proof.
Qed.
Lemma SSu_Sig Γ (A0 A1 : PTm) B0 B1 :
⊨ Γ ->
Γ ⊨ A0 ≲ A1 ->
cons A1 Γ ⊨ B0 ≲ B1 ->
Γ ⊨ PBind PSig A0 B0 ≲ PBind PSig A1 B1.
Proof.
move => hΓ hA hB.
move => hA hB.
have ? : SN A0 /\ SN A1 /\ SN B0 /\ SN B1
by hauto l:on use:SemLEq_SN_Sub.
apply SemLEq_SemWt in hA, hB.