This is the main heuristic used alongside the elim and move lemmas. The goal is to help casts move past operators by adding intermediate casts. An expression of the shape: op (↑(x : α) : γ) (↑(y : β) : γ) is rewritten to: op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ) when (↑(↑(x : α) : β) : γ) = (↑(x : α) : γ) can be proven with a squash lemma
Discharging function used during simplification in the "squash" step.
TODO: normCast takes a list of expressions to use as lemmas for the discharger TODO: a tactic to print the results the discharger fails to prove
Core rewriting function used in the "squash" step, which moves casts upwards and eliminates them.
It tries to rewrite an expression using the elim and move lemmas. On failure, it calls the splitting procedure heuristic.