Stream: Coq users

Topic: ✔ Another rew lemma

Ramkumar Ramachandra (Mar 01 2022 at 20:51):

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

Li-yao (Mar 02 2022 at 00:43):

What's H?

Ramkumar Ramachandra (Mar 02 2022 at 05:37):

H: x = y, where x y: A, P: A -> Type, and B: forall x, P x

Ramkumar Ramachandra (Mar 02 2022 at 08:44):

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.

Ramkumar Ramachandra (Mar 02 2022 at 09:06):

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

Notification Bot (Mar 02 2022 at 18:15):

Ramkumar Ramachandra has marked this topic as resolved.

Last updated: Oct 03 2023 at 02:34 UTC