Hi everyone,

I know a lot of stackoverflow questions are close to this one, but I could not get any proposed solution to work. If one turned out to actually work, I’m sorry for the potential duplicate.

When I define a fixpoint function `my_function`

that does not directly pattern match on its argument `a`

, I cannot unfold it and explicitly see the body of the function in my hypothesis.

Here is a minimal example :

```
Fixpoint my_function (a: nat) :=
if PeanoNat.Nat.eqb a 42 then true
else
match a with
| S a' => my_function a'
| 0 => false end.
Lemma my_lemma:
forall x, my_function x = true -> x >= 42.
Proof.
intros. unfold my_function in H.
(*
at this point, I have:
x : nat
H : (fix my_function (a : nat) : bool :=
if PeanoNat.Nat.eqb a 42 then true else match a with
| 0 => false
| S a' => my_function a'
end) x = true
============================
x >= 42
*)
Abort.
```

After the unfold, my function is not applied to its argument and stays in a strange unapplied form. I would like to have `H`

transformed into:

```
(*
H : if PeanoNat.Nat.eqb x 42 then true else match x with
| 0 => false
| S a' => my_function a'
end = true
*)
```

I don’t want to do this because I not able to prove the result in this case. This is a simplified minimal example of my situation. I know that **destructing the argument** makes Coq apply the function, but in my real case I cannot afford to do the destruct (2 arguments with ~60 constructors). I would like to be able to deal with the `if then else`

cases that are before the pattern matching first, and then destruct the arguments. I can give more details to explain why I would like to do this specific rewrite rather than destructing.

Thank you for your help !

Best,

Clément

PS: I can easily prove a dummy lemma that says that an application of my function is equal to the body, and use it to rewrite. It seems like an ugly solution.

```
Lemma my_function_body:
forall a, my_function a =
if PeanoNat.Nat.eqb a 42 then true
else
match a with
| S a' => my_function a'
| 0 => false end.
Proof.
intros. unfold my_function.
destruct a; reflexivity.
Qed.
```