>>62 の最初の等式

　　　　　　　　　　t
　t　　　　　　　　△
　△　→＜　　t　　 t
t　　i　　　　　△　　△
　　　　　　　t　　　t　　k_i

は >>59 の定義より

△(t, t, k_i) = i
△(t, t, t) = t
△(t, t, t) = t

の３つをまとめて書いた式という意味

この場合、>>25 の代わりに
△(t, t, x) = i を満たす x が存在する、でも確かに OK
一意的な x が存在する、の方がシンプルかもしれないが、
より弱い >>25 の仮定から同じものが導けると考え >>25 を採用したよ

一意性・単射性はとくに使っていないと思うけどどうかな