The key operation on proofs is the substitution of one proof for an assumption used in another proof.
证明的关键操作是用一个证明去替换在另一个证明中使用的假定。