Allow substitutions to passed back from theorems, and to permit assignments "by definition"

[boyland]

The next big urgent change to SASyLF is closer-to-first-class treatment of ":=". Right now inversion and cases can create these, but it would solve a long-standing problem for theorems to be able to "return" these substitutions as well. For example, one could write a subtyping inversion lemma in the following way:

lemma S-Arrow-inversion:
    forall sub: S <: T1 -> T2
    exists T1 <: S1 and S2 <: T2 where S := S1 -> S2
    ...
end lemma

Then someone using the lemma would write:

T1 <: T1' and T2' <: T2 where T := T1' -> T2' by lemma S-Arrow-inversion on sub

The advantage for the user is that they would not need to capture the syntactic identity in an equality relation which would then need to be decoded ("use inversion") on the other end. This removes two steps. And in general, all derivation could be followed by "where" clauses, which would come before the justification (unlike the way inversion permits it now, which would be grandfathered in).
For "use inversion", it would be nice to accept

v := expr by inversion on d

as shorthand for "use inversion on d where v := expr", and in general permit where clauses to occupy the spot for a derivation if a theorem/inversion only produces them, and no derivations.
Separately, it would convenient to permit assignments to introduce a new name, perhaps "by definition":

t0 := fn x:Unit => x by definition

This would be a local analogue to syntax shorthands.

[boyland]

Getting this to work with "or": What would be the way to express n1 = n2 or n1 != n2 without an equality judgment? And/or are desugared into judgments: The first "or" rule in this case would have no premises but would bind n1 and n2. Hmm. So it would have to be (internally at least) something like (() where n1 := n2) or (n1 != n2)