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

Minor cleanup

Browse source
This commit is contained in:
Yiyun Liu 2025-01-30 20:23:57 -05:00
parent fc666956e2
commit d925a8bcaa
1 changed files with 0 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
theories/fp_red.v
View file

@ -144,16 +144,6 @@ 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.
Inductive SNe' {n} : PTm n -> Prop :=
| N_Var' i :
SNe' (VarPTm i)
| N_App' a b :
SNe a ->
SNe' (PApp a b)
| N_Proj' p a :
SNe a ->
SNe' (PProj p a).
Lemma PProjAbs_imp n p (a : PTm (S n)) :
~ SN (PProj p (PAbs a)).
Proof.