[remexre]

That'd require it to be sound and programs to be total: an infinite loop is a proof of anything, and type system unsoundness leads to false proofs