The following minimised example generates 3 unsolved obligations.

```
From Equations Require Import Equations.
Inductive blob : Type := | base.
Variant myeq : blob -> blob -> Type :=
| myrefl {x} : myeq x x.
Derive NoConfusion EqDec for blob.
Derive NoConfusionHom for myeq.
```

I can solve the obligations by essentially aimless elimination until everything becomes trivial, as shown below. However, I think there should be a way to make use of the fact that `blob`

is an h-set to dismiss these obligations, justified by the fact that (I think) dependent elimination "just works" with UIP. What would be the best approach, given that I want to add more inductive constructors to `blob`

and more non-inductive constructors to `myeq`

?

```
Next Obligation.
destruct a.
destruct x.
dependent elimination b1 as [myrefl].
reflexivity.
Defined.
Next Obligation.
destruct a.
destruct x.
dependent elimination b1 as [myrefl].
destruct e.
reflexivity.
Defined.
Next Obligation.
destruct b1.
destruct x.
reflexivity.
Defined.
```

Ah, there's a similar example in the issues (https://github.com/mattam82/Coq-Equations/issues/414), but I'd imagine there too that UIP *for the type of the indices* would be enough.

Last updated: Oct 13 2024 at 01:02 UTC