erwa

erwa is to erw what rwa is to rw: rewrite up to unfolding, then close by assumption.

def CustomPrelude.Tactic.tacticErwa___ : Lean.ParserDescr

erwa is to erw what rwa is to rw.

Equations

• One or more equations did not get rendered due to their size.