DEFINITION terms_props__flat_dec()
TYPE =
       ∀f1:F.∀f2:F.(or (eq F f1 f2) (eq F f1 f2)→∀P:Prop.P)
BODY =
       assume f1: F
          we proceed by induction on f1 to prove ∀f2:F.(or (eq F f1 f2) (eq F f1 f2)→∀P:Prop.P)
             case Appl : ⇒
                the thesis becomes ∀f2:F.(or (eq F Appl f2) (eq F Appl f2)→∀P:Prop.P)
                   assume f2: F
                      we proceed by induction on f2 to prove or (eq F Appl f2) (eq F Appl f2)→∀P:Prop.P
                         case Appl : ⇒
                            the thesis becomes or (eq F Appl Appl) (eq F Appl Appl)→∀P:Prop.P
                               by (refl_equal . .)
                               we proved eq F Appl Appl
                               by (or_introl . . previous)
or (eq F Appl Appl) (eq F Appl Appl)→∀P:Prop.P
                         case Cast : ⇒
                            the thesis becomes or (eq F Appl Cast) (eq F Appl Cast)→∀P:Prop.P
                                suppose H: eq F Appl Cast
                                assume P: Prop
                                  (H0) 
                                     we proceed by induction on H to prove <λ:F.Prop> CASE Cast OF Appl⇒True | Cast⇒False
                                        case refl_equal : ⇒
                                           the thesis becomes <λ:F.Prop> CASE Appl OF Appl⇒True | Cast⇒False
                                              consider I
                                              we proved True
<λ:F.Prop> CASE Appl OF Appl⇒True | Cast⇒False
<λ:F.Prop> CASE Cast OF Appl⇒True | Cast⇒False
                                  end of H0
                                  consider H0
                                  we proved <λ:F.Prop> CASE Cast OF Appl⇒True | Cast⇒False
                                  that is equivalent to False
                                  we proceed by induction on the previous result to prove P
                                  we proved P
                               we proved (eq F Appl Cast)→∀P:Prop.P
                               by (or_intror . . previous)
or (eq F Appl Cast) (eq F Appl Cast)→∀P:Prop.P
                      we proved or (eq F Appl f2) (eq F Appl f2)→∀P:Prop.P
∀f2:F.(or (eq F Appl f2) (eq F Appl f2)→∀P:Prop.P)
             case Cast : ⇒
                the thesis becomes ∀f2:F.(or (eq F Cast f2) (eq F Cast f2)→∀P:Prop.P)
                   assume f2: F
                      we proceed by induction on f2 to prove or (eq F Cast f2) (eq F Cast f2)→∀P:Prop.P
                         case Appl : ⇒
                            the thesis becomes or (eq F Cast Appl) (eq F Cast Appl)→∀P:Prop.P
                                suppose H: eq F Cast Appl
                                assume P: Prop
                                  (H0) 
                                     we proceed by induction on H to prove <λ:F.Prop> CASE Appl OF Appl⇒False | Cast⇒True
                                        case refl_equal : ⇒
                                           the thesis becomes <λ:F.Prop> CASE Cast OF Appl⇒False | Cast⇒True
                                              consider I
                                              we proved True
<λ:F.Prop> CASE Cast OF Appl⇒False | Cast⇒True
<λ:F.Prop> CASE Appl OF Appl⇒False | Cast⇒True
                                  end of H0
                                  consider H0
                                  we proved <λ:F.Prop> CASE Appl OF Appl⇒False | Cast⇒True
                                  that is equivalent to False
                                  we proceed by induction on the previous result to prove P
                                  we proved P
                               we proved (eq F Cast Appl)→∀P:Prop.P
                               by (or_intror . . previous)
or (eq F Cast Appl) (eq F Cast Appl)→∀P:Prop.P
                         case Cast : ⇒
                            the thesis becomes or (eq F Cast Cast) (eq F Cast Cast)→∀P:Prop.P
                               by (refl_equal . .)
                               we proved eq F Cast Cast
                               by (or_introl . . previous)
or (eq F Cast Cast) (eq F Cast Cast)→∀P:Prop.P
                      we proved or (eq F Cast f2) (eq F Cast f2)→∀P:Prop.P
∀f2:F.(or (eq F Cast f2) (eq F Cast f2)→∀P:Prop.P)
          we proved ∀f2:F.(or (eq F f1 f2) (eq F f1 f2)→∀P:Prop.P)
       we proved ∀f1:F.∀f2:F.(or (eq F f1 f2) (eq F f1 f2)→∀P:Prop.P)