Add axioms for finer-grained equational reasoning

[astump]

Andrew proposes axioms like alpha, which just check equivalence without beta-reduction of two terms (eta-expansion too?); and also a one-step reduction proof.

Chris proposes a directional form of beta, which asserts that the lhs of the equation reduces to something alpha-equivalent to the rhs.

Note that the first group of these need to be added to Cedille Core, too.

Also, we should support the Kleene trick for these.

[amarmaduke]

After discussion in a Cedille Developer meeting we decided that because some of these axioms would require changes to Cedille Core that we're going to shelve it for the time being.