次の状況で目標を並べ替える方法を知りたいです。
lemma "P=Q"
proof (rule iffI, (*here I would like to swap goal order*), rule ccontr)
oops
補題ステートメントの変更を伴わない解決策が欲しいです。prefer適用式の証明でも使えると実感しているのですが、その部分deferで使える方法があればいいなと思っています。proof (...)
編集：
Andreas Lochbihler が言うrule iffI[rotated]ように、上記の例では書き込みが機能します。しかし、次のような状況で補題の命題を変えずにゴールの順序を入れ替えることは可能でしょうか?
lemma "P==>Q" "Q==>P"
proof ((*here I would like to swap goal order*), rule ccontr)
oops
この例は不自然に見えるかもしれませんが、補題のステートメントを変更するのは不便である場合や、 などの規則の事前適用がない場合にゴール順序を交換する必要がある場合があると思いますiffI。