(app-of-equal e) equalの適用か (equality focus a b) focusを書き換えられる式 (equality/equation focus concl-inst) 帰結でフォーカスを書き換える conclはきっとconclusionでDethmの法則でいうところの帰結のこと 次の場合、置き換えた結果であるbody(e…