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

Minor

Browse source
This commit is contained in:
Yiyun Liu 2024-12-27 12:15:44 -05:00
parent 7f4c31b14e
commit 1fd0ffe04d
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
theories/fp_red.v
View file

@ -286,10 +286,10 @@ Module RPar.
| ProjCong p a0 a1 : | ProjCong p a0 a1 :
R a0 a1 -> R a0 a1 ->
R (Proj p a0) (Proj p a1) R (Proj p a0) (Proj p a1)
| BindCong A0 A1 B0 B1: | BindCong p A0 A1 B0 B1:
R A0 A1 -> R A0 A1 ->
R B0 B1 -> R B0 B1 ->
R (Pi A0 B0) (Pi A1 B1) R (TBind p A0 B0) (TBind p A1 B1)
| BotCong : | BotCong :
R Bot Bot R Bot Bot
| UnivCong i : | UnivCong i :
@ -404,10 +404,10 @@ Module EPar.
| ProjCong p a0 a1 : | ProjCong p a0 a1 :
R a0 a1 -> R a0 a1 ->
R (Proj p a0) (Proj p a1) R (Proj p a0) (Proj p a1)
| BindCong A0 A1 B0 B1: | BindCong p A0 A1 B0 B1:
R A0 A1 -> R A0 A1 ->
R B0 B1 -> R B0 B1 ->
R (Pi A0 B0) (Pi A1 B1) R (TBind p A0 B0) (TBind p A1 B1)
| BotCong : | BotCong :
R Bot Bot R Bot Bot
| UnivCong i : | UnivCong i :