I’m trying to wrap my brain around the essence of the problems with dependent programming and equality. Some proofs are more difficult or impossible to do without the `JMeq`

axiom. I’ve been trying to formulate a minimal example that captures the essence of this problem:

```
Inductive inf : (unit -> Type) :=
| infc : inf tt -> inf tt.
Lemma match_eq (c : inf tt) (e : tt = tt) :
match e in _ = y return inf y with
| eq_refl => infc c
end = infc c.
```

As far as I can see, this is not provable without axioms. Can anyone confirm this or give a counterexample? The closest I’ve gotten is:

```
refine (
match e as e0 in _ = f return
forall (c0 : inf f),
match e0 in _ = g return inf g with
| eq_refl => infc c
end = infc c0
with
| eq_refl => _
end c).
```

The error message Coq gives here is very confusing by the way. It says that `c0`

in `infc c0`

has type `inf f`

but should have type `inf ()`

. If I then change it to `infc c`

, Coq changes its mind and tells us it `c`

has type `inf ()`

but should have type `inf f`

. This seems to be related to the usage of `unit`

. If I change the argument of `inf`

to `bool`

, the error disappears (but the lemma is still not provable).