Hi. How does one beta-reduce an expression of the form
f x where
f is a finite function in a proof?
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