Building and executing proof strategies in a formal metatheory