Prove the inference system respects alpha-equivalence.

This neat property is enabled by the use of canonical hypothesis lists.
It means that if a sequent is provable, then so is a version of that
sequent with whatever particular choices of alpha-equivalence-class
representatives one desires. Also, one is free to add extraneous
assumptions.

The semantics was already shown to respect alpha, but now the inference
system does too.