On 2013-02-01 22:35, Dmytro Starosud wrote:
> Is there any way to substitute "f refl" with some "g"?
One option, that may or may not work for you, is to switch from Set to a
universe for which a conservative approximation of equality is
decidable. Then you can use an implicit argument of type
True ("decision procedure says yes").
--
/NAD