[atennapel]

If your language has equality proofs, for example `a = Int` then, if your language is non-total I can prove anything by divergence. So I can prove `Int = String`. This is still type-safe as long as you don't erase the proof, because you can never use the invalid proof because your program will diverge.

So if you want to be type-safe but you still want to be able to erase proofs, your proofs have to be total.