暫定的新ゴールの挿入が分からない

Pure等号の推移律はPureの公理（か定理）に入っている。"x == y ==> f x == f z" は示せなかったので、axiomatizationで公理とする。つまり、ファクト（定理データベース）の状況は、

• transitiv: ?x == ?y ==> ?y == ?z ==> ?x == ?y
• eq_preserve: ?x == ?y ==> ?f ?x == ?f ?y

この状況（＝コンテキスト）で、次の命題は簡単に示せると思う。

• "x == y ==> y == z ==> f x == f z"

内容的に同じことをassumes/showsフォーマットで書けば

assumes "x == y" and " y == z"
shows " f x == f z"

ところが、どうするか分からない。中間に "x == z" を挟む操作が分からない。考えられるやり方は、

1. "x == y" と " y == z" からフォーワードリーズニングで "x == z" を出す。
2. "f x == f z" をeq_preserveとユニフィケーションして、バックワードリーズニングで "x == z" を新ゴールとする。

"x == y ==> y == z ==> f x == f z" からスタートするなら、

1. ひとつの命題を、仮定の集合 {"x == y", "y == z"} と、結論 "f x == f z" に分ける。
2. ほんとの結論を保留して、別な命題を仮のゴールに設定する。
3. 新しいゴールを解いて、ローカルなコンテキスト＝仮定の集合に入れる
4. 増えた仮定とバックグラウンド（ローカルコンテキストの外）にある命題を使って元の結論を証明する。

手順を想定できるが、実際の操作が分からない。