DEFINITION F_rec()
TYPE =
Π
P:
F
→
Set
.(P
Appl
)
→
(P
Cast
)
→
Π
f:
F
.(P f)
BODY =
Show proof