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

Prove the soundness of the computable equality

Browse source
This commit is contained in:
Yiyun Liu 2025-03-03 23:46:41 -05:00
parent 36d1f95d65
commit 87f6dcd870
3 changed files with 440 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

5
theories/common.v
View file

@ -1,4 +1,7 @@
Require Import Autosubst2.unscoped Autosubst2.syntax Autosubst2.core ssreflect.
From Equations Require Import Equations.
Derive NoConfusion for nat PTag BTag PTm.
Derive EqDec for BTag PTag PTm.
From Ltac2 Require Ltac2.
Import Ltac2.Notations.
Import Ltac2.Control.
@ -169,4 +172,6 @@ Module HRed.
| IndCong P a0 a1 b c :
R a0 a1 ->
R (PInd P a0 b c) (PInd P a1 b c).
Definition nf a := forall b, ~ R a b.
End HRed.