在AlphaProof使用intro策略后，此时的目的（Goal）为：    这时，AlphaProof使用induction策略，对 n:ℕ进行，归纳证明：    induction策略，在假设中，增加了，在归纳证明中使用的，前值假设，即：    改写后的目的（Goal）的高亮部分，a:∀m<n,