Commit 2020-10-19 22:45 0c70cf30

feat(tactic/unify_equations): add unify_equations tactic (#4515) unify_equations is a first-order unification tactic for propositional equalities. It implements the algorithm that cases uses to simplify indices of inductive types, with one extension: unify_equations can derive a contradiction from 'cyclic' equations like n = n + 1. unify_equations is unlikely to be particularly useful on its own, but I'll use it as part of my new induction tactic.