-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 ฯต ๐ & โf. โโqโ = (โ[q]โซฏf)@โจnโฉ & rโ๐ฑn ฯต t1 &
+ t1[โrโโ[๐ฎโจโbโ๐โqโโฉ](t1โ(pโ๐ฆ))] โ t2