definition ifr (p) (q): relation2 prototerm prototerm ≝
λt1,t2. ∃b.
let r ≝ p●𝗔◗b●𝗟◗q in
- â\88§â\88§ â\8a\93(â\8a\97b) & râ\97\96ð\9d\97±(â\86\91â\9d\98qâ\9d\98) ϵ t1 &
- t2 ⇔ t1[⋔r←↑[𝐮❨↑❘q❘❩]t1⋔(p◖𝗦)]
+ â\88§â\88§ â\8a\97b ϵ ð\9d\90\81 & râ\97\96ð\9d\97±â\9d\98qâ\9d\98 ϵ t1 &
+ t1[⋔r←↑[𝐮❨❘q❘❩](t1⋔(p◖𝗦))] ⇔ t2
.
interpretation