HN Reader

This typechecks:

    function prove_anything<P>(){
        function prove_false() : False {
            return prove_false()
        }
        let f = prove_false()
        return contradiction<P>()(f)
    }

I think a proof assistant will usually have a total notion of computation to avoid this kind of circular proof. And there are probably some subtler unsoundnesses in TS to worry about.

(I'm not any kind of expert in this area. It's possible the original author intends that you execute the proof function as well as typechecking it, which I guess will prove termination, although I think for many proofs you might run out of resources trying to do that, and it's probably still not sound.)