## Stream: Coq users

### Topic: ✔ A rew lemma

#### Ramkumar Ramachandra (Mar 01 2022 at 14:16):

Hi, I'm trying to write a simple `rew` lemma, but I'm stuck here (doesn't type check).

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

#### Gaëtan Gilbert (Mar 01 2022 at 14:20):

the first one should be `rew [fun x => B -> P x]`

#### Ramkumar Ramachandra (Mar 01 2022 at 14:23):

Ah yes! ... but I'm confused now, because my goal doesn't contain that expression in the rew predicate.

/me re-checks

#### Ramkumar Ramachandra (Mar 01 2022 at 15:27):

Okay, I need help help again: doesn't type-check. The lemma is getting out-of-hand.

``````Lemma rew_closure {A} B (P: B -> A -> Type) (Q: B -> Type) {x y: A}
{f: forall (x: A) (ε: B), P ε x} {g: B -> A} (H: x = y):
rew [fun ε x => B -> P ε x] H in (fun (ε: B) => f ε (g ε)) =
fun (ε: B) => rew [P] H in f ε (g ε).
``````

#### Ramkumar Ramachandra (Mar 01 2022 at 15:39):

When applying the original lemma with @Gaëtan Gilbert's fix, I get Unable to unify "?M1379 x" with ... as ... contains local variables.

#### Ramkumar Ramachandra (Mar 01 2022 at 15:42):

x takes epsilon as an argument, so I'm trying to re-work it.

#### Ramkumar Ramachandra (Mar 01 2022 at 16:48):

Never mind. I'll just stick to using `map_subst`.

#### Notification Bot (Mar 01 2022 at 16:48):

Ramkumar Ramachandra has marked this topic as resolved.

Last updated: Oct 03 2023 at 19:01 UTC