Why do I get the following error at the end of the following file? I don't think I can get UIP on `tree A`

without having UIP on `A`

, but I surely do already have `NoConfusion`

for `any`

by the fact that I wrote the relevant `Derive`

command and there didn't seem to be any errors or unsolved obligations at that point.

```
From Equations Require Import Equations.
Inductive tree {A : Type} : Type :=
| zero | plus (s t : tree) | one (x : A).
Arguments tree A : clear implicits.
Derive NoConfusion for tree.
Inductive any {A} {T : A -> Type} : tree A -> Type :=
| here' {x} : T x -> any (one x)
| ll {s t} : any s -> any (plus s t)
| rr {s t} : any t -> any (plus s t).
Arguments any {A} T t.
Derive NoConfusion for any.
Equations here'_inj {A T x t u} : @here' A T x t = here' u -> t = u :=
| eq_refl => eq_refl.
```

```
Error:
[noConfusion] Cannot simplify without UIP on type
(tree A) or NoConfusion for family any
```

You need the homogeneous NoConfusion principle here: `Derive Signature NoConfusionHom for any.`

Thanks! Is the documentation clear on why that is?

And incidentally, is there anything that derives all these injectivity lemmas for me?

I think that the content of the derived NoConfusion(Hom) record is essentially what you are asking for (but in packed form). The documentation isn't ideal on that point (or at least I don't fully understand it).

James Wood has marked this topic as resolved.

Last updated: Jul 24 2024 at 13:02 UTC