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

Add definition for snat

Browse source
This commit is contained in:
Yiyun Liu 2025-02-23 14:07:16 -05:00
parent ffb57a91f4
commit bf6d7db877
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
theories/fp_red.v
View file

@ -212,6 +212,11 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop. Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop.
Inductive SNat {n} : PTm n -> Prop :=
| S_Zero : SNat PZero
| S_Neu a : SNe a -> SNat a
| S_Suc a : SNat a -> SNat (PSuc a)
| S_Red a b : TRedSN a b -> SNat b -> SNat a.
Lemma PProj_imp n p a : Lemma PProj_imp n p a :
@ishf n a -> @ishf n a ->