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 ε).
```

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

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

/me re-checks

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 ε).
```

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

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

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

.

Ramkumar Ramachandra has marked this topic as resolved.

Last updated: Jan 31 2023 at 12:01 UTC