The key is &quot;forall f&quot;. That is, this must hold for all functions.  In a constructive world, the set of all functions is finite.  There&#x27;s an existing set of known functions on the object.  Any new functions must be created using those functions, so if the known functions have that property, so must functions built from them.<p>The key idea is that new functions can&#x27;t look inside the object directly.  Think private data and function members in C++.  So two objects may have different internal representations, but if the exported functions won&#x27;t let you distinguish them, you can treat them as equal.