Refinement Functions

refine: rule tactic.

This function refines a proof according to a given rule.

refine_using_prl_rule: tok tactic.

This function parses the token as a rule in the context of the given proof. The proof is then refined via this rule.