Hi, I've been medling with defining recursive function with an explicit measure via `Fix`

,

and I've stumbled into a bit of a roadblock when trying to prove an unfolding lemma `Fix _ _ F x = F x _ (Fix _ _ F)`

.

I use std++'s lemma `Fix_unfold_rel`

. This works fine and the goal it generates seems highly reasonable,

Here is a minimal example:

```
Lemma dep_match_eq {A} (f : A -> option A)
(g h : ∀ x y, f x = Some y -> A)
(Hgh : ∀ x y H, g x y H = h x y H) x :
match f x as x' return f x = x' -> A with
| Some y => fun Heq => g x y Heq
| None => fun _ => x
end eq_refl =
match f x as x' return f x = x' -> A with
| Some y => fun Heq => h x y Heq
| None => fun _ => x
end eq_refl.
```

Now I can prove this by using the functional extensionality axiom to show `g = h`

, then rewrite and use reflexivity. However it seems like it should be provable without. Is there any way I can achieve this ? or alternatively, a better way to do this ?

(I can provide a more complete example if need be, but I think this here is the gist of my problem)

Ok I see... It indeed the same problem (I really want to `destruct (f x)`

, but I can't.

A friend help me find a solution that work by generalizing:

```
Proof.
remember (g x).
remember (h x).
pose (Hgh x).
rewrite <- Heqa in e.
rewrite <- Heqa0 in e.
clear g h Hgh Heqa Heqa0.
destruct (f x).
- auto.
- auto.
Qed.
```

Last updated: Jun 18 2024 at 10:02 UTC