I have some code like this

```
Lemma foo : P (f ...).
```

Where `f`

varies, I'm looking for a ltac way of unfolding f, I tried match goal but it doesn't work as I expect

```
Parameter Foo : forall {a : Set}, a -> Prop.
Definition f {A : Set} (x : A) := x.
Lemma foo {A : Set} (x : A) : Foo (f x).
Proof.
match goal with
| |- Foo (?g _) => unfold g
end.
```

In my case `f`

will have arbitrary number of arguments, I don't want to match to the number of the arguments, I want to match to an application of a function to any number of arguments greater or equal to 1. Something like `g _ `

`g _ _`

`g _ _ _ ...`

```
Ltac head f :=
match f with
| ?g _ => head g
| _ => f
end.
Lemma foo {A : Set} (x : A) : Foo (f x).
Proof.
match goal with
| |- Foo ?g => let g := head g in unfold g
end.
```

Thank you Guillaume I'm adapting to my real-world case :)

Daniel Hilst Selli has marked this topic as resolved.

I just realize that I could have used `Hint Unfold f : foo_db`

and then `autounfold with foo_db`

:face_palm:

Last updated: Jun 17 2024 at 22:01 UTC