DEFINITION F_ind()
TYPE =
       ∀P:F→Prop.(P Appl)→(P Cast)→∀f:F.(P f)
BODY =
        assume P: F→Prop
        suppose H: P Appl
        suppose H1: P Cast
        assume f: F
          by cases on f we prove P f
             case Appl ⇒
                the thesis becomes the hypothesis H
             case Cast ⇒
                the thesis becomes the hypothesis H1
          we proved P f
       we proved ∀P:F→Prop.(P Appl)→(P Cast)→∀f:F.(P f)