Yes they do. In a supremely roundabout way typically making for ugly fat proofs for anything high order. Sometimes, rarely, they make proofs cleaner and more di

Yes they do. In a supremely roundabout way typically making for ugly fat proofs for anything high order. Sometimes, rarely, they make proofs cleaner and more direct than high order logic. Plus there is the potential undecidability if you want to use automated type deduction. Hard to spot where the types have to be so to speak reified with bad error messages.