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.
Last updated: Feb 08 2023 at 07:02 UTC