Hi. How does one beta-reduce an expression of the form `f x`

where `f`

is a finite function in a proof?

I tried `cbn`

, `hnf`

and `simpl`

and none works.

I even tried with

```
change ([ffun k0 => if fsval k0 \in ks
then v
else odflt v m.[? fsval k0]]
(fincl ks_sub [` H]))
with (if fsval (fincl ks_sub [` H]) \in ks
then v
else odflt v m.[? fsval (fincl ks_sub [` H])]).
```

and didn't work. That's suspicious.

I found it! `rewrite ffunE`

does the trick.

Ricardo has marked this topic as resolved.

Last updated: Nov 29 2023 at 05:01 UTC