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-25 01:24:56 -05:00
parent c0faae5d8a
commit 3cb40ccb9e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
theories/fp_red.v
View file

@ -881,7 +881,7 @@ Proof.
Qed. Qed.
Local Ltac prov_tac := sfirstorder use:depth_ren. Local Ltac prov_tac := sfirstorder use:depth_ren.
Local Ltac extract_tac := sfirstorder use:depth_subst_bool. Local Ltac extract_tac := rewrite -?depth_subst_bool;hauto use:depth_subst_bool.
#[tactic="prov_tac"]Equations prov {n} (A : Tm n) (B : Tm (S n)) (a : Tm n) : Prop by wf (depth_tm a) lt := #[tactic="prov_tac"]Equations prov {n} (A : Tm n) (B : Tm (S n)) (a : Tm n) : Prop by wf (depth_tm a) lt :=
prov A B (Pi A0 B0) := rtc Par.R A A0 /\ rtc Par.R B B0; prov A B (Pi A0 B0) := rtc Par.R A A0 /\ rtc Par.R B B0;