isabelle - 伊莎贝尔：选择假设/选择目标/指定元变量

Question

1）如何选择我想在 Isabelle/FOL 定理中应用的假设？

有一个证明案例，我不能使用“应用假设”。

 axiomatization
  where aax8  : ‹(A-->C)-->(B-->C)-->(A∨B-->C)›
    and aax11 : "A∨~A"

lemma ewfw : ‹ ⟦(A-->B); ~A-->B⟧==>B›
  apply(rule mp)
   apply(rule mp)
  apply(rule mp)
     apply(rule aax8)

    apply assumption
  ???
  done

我有这种交互式证明状态的情况：

proof (prove)
goal (2 subgoals):
 1. (A --> B) ==> (¬ A --> B) ==> (?B9 --> B)
 2. (A --> B) ==> (¬ A --> B) ==> (A ∨ ?B9)

解决这个问题的另一种方法是选择另一个目标。

2) 如何选择我接下来要证明的目标？

另一种方法是用公式“〜A”用问号（？B9）替换变量，所以

3）如何在证明过程中用公式指定元变量？