Arvid@dexter lemmas and refactorings
This MR adds some innocuous lemmas and moves the fold_eval_precond tactic to a more practical place.
This is used by dexter in !100
This MR adds some innocuous lemmas and moves the fold_eval_precond tactic to a more practical place.
This is used by dexter in !100