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

(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.)