Expose proofstate's Empty constructor in rules #12
Description
Tactics can use alternative empty, but rules have no recourse. Suggest calling it cut and making it tactic/rule polymorphic.
{{ message }}
Tactics can use alternative empty, but rules have no recourse. Suggest calling it cut and making it tactic/rule polymorphic.