DEFINITION F_ind()
TYPE =
∀
P:
F
→
Prop
.(P
Appl
)
→
(P
Cast
)
→
∀
f:
F
.(P f)
BODY =
Show proof