This file contains general-purpose proof tactics that are shared across the Cedar theorems and not tied to any specific subsystem. #
This tactic simplifies assumptions of the form do (let x ← expr ...) by
performing a cases and simp on expr.
Optionally, as h names the case-analysis hypothesis (avoiding a subsequent rename_i).
Equations
- One or more equations did not get rendered due to their size.