```
Structure test A B (H: A = B) := {
t: forall (x: A) (y: B), x = y
}.
```

Let's use this as toy example. How to tell Coq that `A = B`

and therefore `x = y`

makes sense?

Solved.

```
Structure test A B (H: A = B) := {
t: forall (x: A) (y: B), eq_rect _ _ x _ H = y
}.
```

Lessness has marked this topic as resolved.

There's also the `rew`

notation, which imo looks nice here:

```
Import EqNotations.
Structure test A B (H: A = B) := {
t: forall (x: A) (y: B), rew H in x = y
}.
```

Last updated: Oct 13 2024 at 01:02 UTC