Commit 2020-12-30 08:01 1c110ada

fix(tactic/linarith): elaborate and insert arguments before destructing hypotheses (#5501) closes #5480 Arguments to linarith can depend on hypotheses (e.g. conjunctions) that get destructed during preprocessing, after which the arguments will no longer elaborate or typecheck. This just moves the elaboration earlier and adds these arguments as hypotheses themselves.