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: Jun 15 2024 at 05:01 UTC