"you can rewrite every function type A → B to its CPS version A → (B ↠ #) ↣ #"
where you throw the continuation (B ↠ #) on the left, which then consumes its argument to the right... but this falls over because at some stage you'll want to construct a continuation (which only puts an ordered hypothesis A into the context) which calls a real function, which needs a real (unrestricted) value for an argument. It's even worse if you keep function-argument-values and intermediate-stack-values separate, as I did in my last twelf encoding.
And yet the twelf encoding seems to work! Bijectively, even! This suggests to me that there's some logic that describes the output of the translation, even if it isn't straightforward ordered logic, or at least it doesn't translate function types like I conjectured above. What's going on?