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

Add prov function (WIP)

Browse source
This commit is contained in:
Yiyun Liu 2024-12-24 01:19:42 -05:00
parent 46ec21b763
commit c6edc1b0be
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
theories/fp_red.v
View file

@ -752,6 +752,14 @@ Proof.
sfirstorder use:relations.diamond_confluent, EPar_diamond. sfirstorder use:relations.diamond_confluent, EPar_diamond.
Qed. Qed.
Fixpoint prov {n} A B (a : Tm n) : Prop :=
match a with
| Pi A0 B0 => rtc Par.R A A0 /\ rtc Par.R B B0
| App a b => prov A B a
| Abs a => prov A B (subst_Tm (scons A VarTm) a)
| _ => True
end.
Lemma Par_confluent n (c a1 b1 : Tm n) : Lemma Par_confluent n (c a1 b1 : Tm n) :
rtc Par.R c a1 -> rtc Par.R c a1 ->
rtc Par.R c b1 -> rtc Par.R c b1 ->