Struggling with Traced

This is just bunch of commented out code, that I am struggling with.
I can see how this one should hold.  From the well foundedness we can
get `b₁` and `b₂` which bundled with input could be fed to the
function `f` and leter projected away.  However this means that the
sides of `cong` operation are _slightly_ different.