Hi ! How can I discriminate equalities like

```
Heq_l : Nnil ~= Ncons x l
```

where `Nnil`

and `Ncons`

are dependent list constructors ?

what's ~=

I think this is the one, in `Program.Equality`

:

```
Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
```

one way to work with assumptions that use `JMeq`

is to apply `JMeq_eq`

(uses axiom `Eqdep.Eq_rect_eq.eq_rect_eq`

on recent Coq), then they become a normal equality.

It seems not sufficient in this case because both sides don't have the same type for `JMeq_eq`

to be applicable.

Last updated: Jun 23 2024 at 01:02 UTC