```
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: Jul 15 2024 at 20:02 UTC