T : eqType
p1, p2 : pred T
============================
[pred x | p1 x == p2 x] = [pred x | p2 x == p1 x]
I think about some kind of rewrite under
but what kind the under
equation do I need?
If you state it with =1
then it is provable without axioms. A pred is just a function to bool, your goal is very strong in type theory.
@Enrico Tassi , thank you very much.
Last updated: Mar 29 2024 at 15:02 UTC