Sometimes I need to define an inductive proposition of the following form:
Inductive foo : A -> B -> Prop := | Foo : forall c, foo a0 (f c).
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
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!