B.4 Secondary Commands

B.4 Secondary Commands

This section lists those commands that are typically applied in the middle phase of constructing a proof; they require creativity from the user to determine the right proof strategy and to guide the system towards a successful proof completion.

• B.4.1 I:T=E: Declare Value
• B.4.2 assume: Use and Prove Assumption
• B.4.3 case: Perform Case Distinction
• B.4.4 expand: Expand Definitions
• B.4.5 flip: Flip Formula
• B.4.6 goal: Make Formula Goal
• B.4.7 instantiate: Instantiate Variables in Formula
• B.4.8 lemma: Import Lemmas
• B.4.9 typeaxiom: Instantiate Type Axiom

B.4 Secondary Commands