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

Add a possible fix

Browse source
This commit is contained in:
Yiyun Liu 2025-01-04 01:40:38 -05:00
parent 162db5296f
commit 68207eb3bd
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
theories/fp_red.v
View file

@ -1064,6 +1064,7 @@ Definition prov_univ {n} i0 (a : Tm n) :=
(* Can consider combine prov and provU *) (* Can consider combine prov and provU *)
#[tactic="prov_tac"]Equations prov {n} (h : Tm n) (a : Tm n) : Prop by wf (depth_tm a) lt := #[tactic="prov_tac"]Equations prov {n} (h : Tm n) (a : Tm n) : Prop by wf (depth_tm a) lt :=
prov h (TBind p0 A0 B0) := prov_bind p0 A0 B0 h; prov h (TBind p0 A0 B0) := prov_bind p0 A0 B0 h;
(* Try forall b, prov h (a {b /x})? *)
prov h (Abs a) := prov (ren_Tm shift h) a; prov h (Abs a) := prov (ren_Tm shift h) a;
prov h (App a b) := prov h a; prov h (App a b) := prov h a;
prov h (Pair a b) := prov h a /\ prov h b; prov h (Pair a b) := prov h a /\ prov h b;