-inductive ifr (p) (q) (t): predicate preterm โ
-| ifr_beta (b):
- let r โ pโ๐โbโ๐โq in
- rโ๐ฑโจโโqโโฉ ฯต t โ โโb โ ifr p q t (t[โrโโ[๐ฎโจโโqโโฉ]tโ(pโ๐ฆ)])
+definition ifr (p) (q): relation2 prototerm prototerm โ
+ ฮปt1,t2. โโb,n.
+ let r โ pโ๐โbโ๐โq in
+ โงโง โb ฯต ๐ & โqโ = (โ[q]๐ข)@โจnโฉ & rโ๐ฑn ฯต t1 &
+ t1[โrโโ[๐ฎโจnโฉ](t1โ(pโ๐ฆ))] โ t2