SDPE との関係: HOAS を用いた SDPE
R(?(?x. t)) = ?(?y. R((?x. t) @ y))
R(t1 @ t2) = (?x. t) @ R(t2) (if R(t1) = ?(?x. t))
R(t1 @ t2) = R(t1) @ R(t2) (otherwise)
??(?x. t) = ?(?y. (?x. t) @ y)
t1 @? t2 = (?x. t) @ t2 (if t1 = ?(?x. t))
t1 @? t2 = t1 @ t2 (otherwise)