結論から言うと、質問で悩んでいる部分は「二階（高階）マッチング」の、ごく限定された特別ケースになっています。
今回のように φ は引数一つ z を持つ式 φ(z) で、その「いくつかの具体値 ti を代入した結果」が与えられているだけなら、次のような「構文木を平行に見ていく」アルゴリズムで判定できます。
◆前提の整理
公理７は
∀x ∀y ((x = y) ⇒ (φ[x/z] ⇒ φ[y/z]))
の形をしています。
ここで φ は一変数のメタ変数（φ(z)）だと思っておき、φ[x/z] は φ(z) の z に x を代入した結果 φ(x)、φ[y/z] は φ(y) だと見なします。
与えられた具体的な式
∀t ∀u ((t = u) ⇒ ((t = t) ⇒ (u = t)))
がこのインスタンスかどうかを判定したい、という問題です。
◆大きな流れ
1. まず、φ の中身を無視して「骨組み」だけ一階のパターンマッチをする。
2. その結果として、「φ[x/z] に対応する具体式 F1」「φ[y/z] に対応する具体式 F2」が取れる。
3. 次に、「ある一変数式 Φ(z) があって、Φ(x) = F1, Φ(y) = F2 となるか」を構文木を用いて調べる。
これがうまく行けば、その Φ が φ であり、元の式は公理７のインスタンス、と判定できる。
順に説明します。
1. 骨組みの一致を見る（φ をブラックボックス扱い）
φ[x/z], φ[y/z] の部分を「何かの命題記号」としてとりあえず潰してしまいます。例えば
∀x ∀y ((x = y) ⇒ (φ[x/z] ⇒ φ[y/z]))
の φ[x/z] を P、φ[y/z] を Q という０項述語のような記号に置き換えると
∀x ∀y ((x = y) ⇒ (P ⇒ Q))
になります。
同じように、候補式
∀t ∀u ((t = u) ⇒ ((t = t) ⇒ (u = t)))
の中で、P に対応しそうな部分、Q に対応しそうな部分を探します。
量化子と最外の ⇒ の形は完全に一致しているので、
x ↔ t, y ↔ u, P ↔ (t = t), Q ↔ (u = t)
と対応付けられます。
この時点で「公理７の骨組み」と「候補式の骨組み」は一致しています。
よって、次の問題に還元されます。
ある Φ(z) が存在して、
Φ(x) = (x に対応する t を代入した結果) = (t = t)
Φ(y) = (y に対応する u を代入した結果) = (u = t)
となるか
つまり
Φ(x) = t = t
Φ(y) = u = t
を満たす Φ が存在するかどうかを調べれば良い。
2. φ を逆に「復元」するアルゴリズム（多重代入の場合）
ここからが質問の核心で、「代入が複数回ある」場合の一般的な考え方です。
今、
・未知の一変数式 Φ(z)
・既知の項 t1, t2, …, tn
・既知の式 F1, F2, …, Fn
があり、「すべての i について Φ(ti) = Fi」としたい、という状況だとします。
今回の例では n = 2, t1 = x ↦ t, t2 = y ↦ u, F1 = (t = t), F2 = (u = t) です。
アルゴリズムは「Fi 同士の構文木を平行にたどりながら z の位置を見つける」イメージです。
(1) まず一つ目の式 F1 の構文木を基準にする。
今回は F1 = (t = t) なので、「根は =、左右の子を t, t に持つ木」です。
(2) 同じ位置を他の Fi でも見る。
F2 = (u = t) も根は = で左右の子を u, t に持ちます。
根の記号（=）は全ての Fi で一致しているので、Φ(z) も「= を根に持つ式」であるはず、と分かります。
よって Φ(z) は「左の引数部分」「右の引数部分」に分けて調べられます。
(3) 左の引数のペアを調べる。
F1 の左引数は t, F2 の左引数は u なので、(t, u) という組です。
一般には (t1′, t2′, …, tn′) という形になりますが、ここでは n = 2 です。
この位置が「z を代入した結果になっている」と仮定すると、
t1′ = t1 に相当する項（今回なら t）
t2′ = t2 に相当する項（今回なら u）
となっていなければいけません。
実際、
t1′ = t は「x に対応する t」と一致
t2′ = u は「y に対応する u」と一致
するので、この位置を「z が現れている位置」とみなせます。
つまり、Φ(z) の左引数は「z」であることがわかる。
(4) 右の引数のペアを調べる。
F1 の右引数は t, F2 の右引数も t で、両方とも同じ記号 t です。
ここには z の影響が出ていないので、「Φ(z) の右側は常に t」とみなせます。
以上から、
Φ(z) = (z = t)
と復元できます。
この Φ(z) に対して、
Φ(x) = (x = t) だが、x は t に対応しているので (t = t)
Φ(y) = (y = t) だが、y は u に対応しているので (u = t)
となり、確かに F1, F2 を再現しています。
よって、
φ[z] ≡ (z = t)
とおけば、候補式は公理７のインスタンスだと判定できます。
3. 一般化の仕方のポイント
今の手続きを少し抽象化すると、次のようになります。
(1) 公理図式側の φ[ti/z] それぞれに対応して、具体式側から Fi を取り出す。
これ自体は、φ を一時的に新しい記号に見立てた一階のパターンマッチでできる。
(2) 集めた対の集合 {(ti, Fi)} を使って、「ある一変数式 Φ(z) があって Φ(ti) = Fi がすべて成り立つか」を判定する。
判定は構文木に対する再帰で行う。
具体的には:
・全 Fi の根記号が同じ論理記号・述語記号なら、その記号を根とする形に Φ を仮定し、各引数ごとに再帰する。
・ある位置で「全ての Fi のその位置の項が ti に対応するものになっている」なら、その位置を z とみなす。
・どの位置もそうならないし、かつ Fi の記号が食い違う場合は失敗（そのような Φ は存在しない）。
ここで重要なのは、φ が「z だけを自由変数に持つ式」として扱えることです。
もし φ が複数の自由変数を持ったり、φ 自身が他のメタ変数の内部に現れたりすると、一般には二階・高階の単一化になり、決定不能な場合も出てきます。
しかし、通常の一階述語論理の公理図式では、φ は「自由変数が決まっている単純なメタ変数」でしか出てこないので、上のような単純な構文木の平行走査で十分です。
4. 質問に対するまとめ
・「代入が一回」の場合にやっていた「差異部分を hole にする」やり方は、「Φ(z) を構文木として復元する」という観点から自然に一般化できる。
・「代入が二回以上」の場合は、「複数の Fi を同時に見て、どこが z の位置かを一貫して決められるか」を見る問題になる。
・実際のアルゴリズムは、複数の Fi の構文木を平行に走査し、全ての i で同じ記号が現れている所は φ の固定部分、ti のパターン通りにしか変化しない所は z の位置、として Φ(z) を組み立てていく。
・この手続きで Φ(z) を一意に復元できれば、その候補式は元の公理図式のインスタンスだと判定できるし、途中で矛盾が出ればインスタンスではないと分かる。
こんな形で、「φ を一変数関数 Φ(z) とみなして、複数の代入結果から逆算する」と考えると、代入が二回以上ある場合でも機械的な判定アルゴリズムが作れます。
