<div dir="ltr"><div><div>```<br>module Test2 where<br><br><br>data A : Set where<br><br><br>CPF : Set<br>CPF = {{a : A}} → A<br><br>postulate<br>  fun : CPF → CPF<br>  e : CPF<br>  <br><br>bob : CPF<br>bob {{ctx}} = fun (e {{ctx}})<br><br><br>rob : CPF<br>rob = fun e <br><br>```<br><br></div>I wonder if there is a way to write "rob" instead of "bob".<br><br></div>Keep in mind that the candidates are definitionally equal. (it seems)<br></div>