Hello,

Sometimes I need to define an inductive proposition of the following form:

```
Inductive foo : A -> B -> Prop :=
| Foo : forall c, foo a0 (f c).
```

where `a0 : A`

and `f : C -> B`

.

The issue is that when trying to prove a statement of the form `foo a b`

if I want to `apply Foo`

I need to first `assert`

that `a = a0`

and `b = f c`

for some `c`

. Is there a way to “apply” `Foo`

and automatically deduce new goals with the required equalities ?

I could include the equalities in the definition of the inductive type, as in:

```
Inductive foo : A -> B -> Prop :=
| Foo : forall a b c,
a = a0 ->
b = f c ->
foo a b.
```

but this feels very inelegant. Is there another way?

Any suggestions appreciated. Thanks!

Best wishes,

Nicolás