Document `iRewrite -...` in `ProofMode.md`
I would like to be able to say something like iRewrite <- "Heq"
so that it would transform the goal
"Heq": R ≡ Q
-------------*
Q
into
-------------*
R
I would like to be able to say something like iRewrite <- "Heq"
so that it would transform the goal
"Heq": R ≡ Q
-------------*
Q
into
-------------*
R