Clean up implementation such that unused proofs terms are not carried around

[L-as]

Certain types are morally in Prop. We can rewrite the code such that they don't exist at run-time.