I'd like to prove a lemma that looks vaguely like this:

```
Lemma example (T : finType) (n : nat) (f : {dffun forall k : 'I_n.+1, k.-tuple T}) :
f = [ffun k : 'I_n.+1 => f (id k)].
```

I expected it would be enough to prove extensional equality, and in fact there is `eq_ffun`

:

```
eq_ffun : forall g1 g2 : ?aT -> ?rT,
g1 =1 g2 -> [ffun x => g1 x] = [ffun x => g2 x]
```

However the `g1`

and `g2`

are "regular" functions instead of finite functions. I figured it would be alright due to the coercion, but apparently not:

```
Fail rewrite eq_ffun.
(*
Error: The LHS of eq_ffun
[ffun x => _ x]
does not match any subterm of the goal
*)
```

and:

```
Fail rewrite (eq_ffun (fun_of_fin f)).
(*
The term "fun_of_fin f" has type
"forall x : ordinal_finType n.+1, x.-tuple T"
while it is expected to have type
"ordinal_finType n.+1 -> ?rT" (cannot instantiate
"?rT" because "x" is not in its scope: available arguments
are "T" "n" "f").
*)
```

It looks like the coercion is not applicable because `f`

has a dependent type. Is there a way around this?

`apply/ffunP`

Thanks Cyril!

Last updated: Jul 25 2024 at 15:02 UTC