Elimination fixes

[joshcbrown]

This mainly does two things:

1. When substituting in higher order terms, perform a reduction on the substituted result. We need this with elimination because the flow looks like:
   i. Unify rule's conclusion with assumption, get a substitution
   ii. Substitute rule with substitution from previous step
   iii. Unify newly substituted rule with goal
   If after ii. we don't reduce, the shapes are different but the same modulo reduction owing to the magic way higher order unification works. @mio-19 is this an OK change? Could the reduction be performed somewhere else?
2. Add extra filters for assumptions & rules to exclude variables where they might cause problems

[joshcbrown]

I forgot that reduce was made a part of the signature of TERM. It therefore isn't necessary for this fix to move the reduction to the end of substitution---we can just do the reduction at the call site when searching for eliminations---though now I'm wondering whether that's a sensible thing to do regardless?

[mio-19]

we can just do the reduction at the call site when searching for eliminations

reduce after subst is also used in some existing code

holbert-ng/src/Rule.res

Line 26 in 3c5c7e5

->Judgment.reduce,

[joshcbrown]

I guess a question is then: might you ever want to interact with a substituted but not-reduced HOTerm.t? If not, we can move that reduction to inside the definition of substDeBruijn in HOTerm too.

[mio-19]

I guess a question is then: might you ever want to interact with a substituted but not-reduced HOTerm.t? If not, we can move that reduction to inside the definition of substDeBruijn in HOTerm too.

substDeBruijn is currently referenced by the unification algorithm. I definitely want to avoid calling expensive reduce in the unification algorithm

[joshcbrown]

Got it, fair enough! I'll do the reduction in Rule then to keep it consistent