Is this provable? `fun 𝛉 => (rew [P 𝛉] H in B 𝛉) = rew [forall 𝛉, P 𝛉] H in B.`

What's `H`

?

`H: x = y`

, where `x y: A`

, `P: A -> Type`

, and `B: forall x, P x`

Finally, I went with this, that Hugo wrote me:

```
Lemma map_subst_app {A B} {a: A} {x y} (H: x = y :> B) (C: A -> B -> Type)
(f: forall a, C a x):
rew [C a] H in f a = (rew [fun x => forall a, C a x] H in f) a.
```

Sigh, hitting https://github.com/coq/coq/issues/15517 again -- I hit it all the time :(

Ramkumar Ramachandra has marked this topic as resolved.

Last updated: Jan 29 2023 at 05:03 UTC