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

Remove funext from Equations

Browse source
This commit is contained in:
Yiyun Liu 2024-12-25 19:59:13 -05:00
parent 22c7eff954
commit 98a11fb7ac
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
theories/fp_red.v
View file

@ -10,6 +10,8 @@ From Hammer Require Import Tactics.
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax.
From Equations Require Import Equations. From Equations Require Import Equations.
Unset Equations With Funext.
Ltac2 spec_refl () := Ltac2 spec_refl () :=
List.iter List.iter
(fun a => match a with (fun a => match a with
@ -1039,7 +1041,8 @@ Lemma ren_extract n m (a : Tm n) (ξ : fin n -> fin m) :
Proof. Proof.
move : m ξ. elim : n/a. move : m ξ. elim : n/a.
- sfirstorder. - sfirstorder.
- move => n a ih m ξ. simpl. simp extract. - move => n a ih m ξ. simpl.
simp extract.
rewrite ih. rewrite ih.
by asimpl. by asimpl.
- hauto q:on rew:db:extract. - hauto q:on rew:db:extract.
@ -1100,6 +1103,7 @@ Proof.
- qauto rew:db:prov. - qauto rew:db:prov.
Qed. Qed.
Lemma prov_par n (A : Tm n) B a b : prov A B a -> Par.R a b -> prov A B b. Lemma prov_par n (A : Tm n) B a b : prov A B a -> Par.R a b -> prov A B b.
Proof. Proof.
move => + h. move : A B. move => + h. move : A B.