Hi,

So far in my development, I've mostly used UIP, with `Require Import EqDep`

. I also use `Program.Equality`

for `dependent destruction`

. However, I'm now thinking of switching to requiring proof irrelevance with `Require Import ProofIrrelevance`

. However, it seems to me like `Require Import Program.Equality`

will always import the plain UIP `eq_rect_eq`

axiom, which means I will have both proof irrelevance and UIP as separate axiom without one being defined from the other. Is that a problem? Is there a way to solve this?

I don't know of a solution but I can't imagine how that could be a problem in practice.

One solution is to use `Equations`

instead of Program because you can provide your own instance of UIP. But indeed, you probably don't have a real problem to begin with.

in many cases, I think the Equations tactics can also avoid using `eq_rect_eq`

for dependent elimination/destruction

Last updated: Jun 23 2024 at 04:03 UTC