Proof that subst preserves errors

[cdisselkoen]

The next lemma required for PE soundness. We already have a lemma stating that "if partial evaluation returns a concrete value, then it returns the same concrete value after any substitution of unknowns [in the original expression/request/entity store]". This is the counterpart for when partial evaluation returns an error.

Notably, the statement is not that partial evaluation must return the same error after any substitution of unknowns; that doesn't hold (one of many counterexamples: principal.foo + false where the principal is initially unknown, but the substitution maps it to some entity which doesn't have a foo attribute. This gives a type error before substitution, but an attrDoesNotExist error after substitution.) Instead, the statement is that partial evaluation must return some error (not necessarily the same error) after any substitution of unknowns.

As of this writing, I have not yet normalized the simps in this PR.

[khieta]

Overall structure and theorem statement seems fine to me. Approving as-is, though I imagine you'll still do some hacking on the proofs (e.g., normalizing simps)

[khieta]

Why _mt?

[cdisselkoen]

From the Latin "modus tollens", which in formal logic is the rule for contrapositives. I named this in analogue to Lean's use of mp (from the Latin "modus ponens") to mean the forward direction of an implication. Suggestions for a different name? I suppose _contrapositive?

[emina]

Looks good to me.