tirix / rumm

A tactics-based Metamath proof language
4 stars 3 forks source link

typo #10

Closed GinoGiotto closed 7 months ago

GinoGiotto commented 7 months ago

The apply tactic requires a statement label after with. Therefore, if I want to specify the substitution for ps, I need to provide its corresponding label, which in this case is wps.