DEFINITION aprem_gen_head_O()
TYPE =
       ∀a1:A.∀a2:A.∀x:A.(aprem O (AHead a1 a2) x)→(eq A x a1)
BODY =
        assume a1: A
        assume a2: A
        assume x: A
        suppose H: aprem O (AHead a1 a2) x
           assume y: A
           suppose H0: aprem O y x
              assume y0: nat
              suppose H1: aprem y0 y x
                we proceed by induction on H1 to prove (eq nat y0 O)→(eq A y (AHead a1 a2))→(eq A x a1)
                   case aprem_zero : a0:A a3:A ⇒
                      the thesis becomes (eq nat O O)→∀H3:(eq A (AHead a0 a3) (AHead a1 a2)).(eq A a0 a1)
                          suppose : eq nat O O
                          suppose H3: eq A (AHead a0 a3) (AHead a1 a2)
                            (H4) 
                               by (f_equal . . . . . H3)
                               we proved 
                                  eq
                                    A
                                    <λ:A.A> CASE AHead a0 a3 OF ASort  ⇒a0 | AHead a ⇒a
                                    <λ:A.A> CASE AHead a1 a2 OF ASort  ⇒a0 | AHead a ⇒a

                                  eq
                                    A
                                    λe:A.<λ:A.A> CASE e OF ASort  ⇒a0 | AHead a ⇒a (AHead a0 a3)
                                    λe:A.<λ:A.A> CASE e OF ASort  ⇒a0 | AHead a ⇒a (AHead a1 a2)
                            end of H4
                            (H6) 
                               consider H4
                               we proved 
                                  eq
                                    A
                                    <λ:A.A> CASE AHead a0 a3 OF ASort  ⇒a0 | AHead a ⇒a
                                    <λ:A.A> CASE AHead a1 a2 OF ASort  ⇒a0 | AHead a ⇒a
eq A a0 a1
                            end of H6
                            consider H6
                            we proved eq A a0 a1
(eq nat O O)→∀H3:(eq A (AHead a0 a3) (AHead a1 a2)).(eq A a0 a1)
                   case aprem_succ : a0:A a:A i:nat H2:aprem i a0 a a3:A ⇒
                      the thesis becomes ∀H4:(eq nat (S i) O).∀H5:(eq A (AHead a3 a0) (AHead a1 a2)).(eq A a a1)
                      (H3) by induction hypothesis we know (eq nat i O)→(eq A a0 (AHead a1 a2))→(eq A a a1)
                          suppose H4: eq nat (S i) O
                          suppose H5: eq A (AHead a3 a0) (AHead a1 a2)
                            (H6) 
                               by (f_equal . . . . . H5)
                               we proved 
                                  eq
                                    A
                                    <λ:A.A> CASE AHead a3 a0 OF ASort  ⇒a3 | AHead a4 ⇒a4
                                    <λ:A.A> CASE AHead a1 a2 OF ASort  ⇒a3 | AHead a4 ⇒a4

                                  eq
                                    A
                                    λe:A.<λ:A.A> CASE e OF ASort  ⇒a3 | AHead a4 ⇒a4 (AHead a3 a0)
                                    λe:A.<λ:A.A> CASE e OF ASort  ⇒a3 | AHead a4 ⇒a4 (AHead a1 a2)
                            end of H6
                            (h1) 
                               (H7) 
                                  by (f_equal . . . . . H5)
                                  we proved 
                                     eq
                                       A
                                       <λ:A.A> CASE AHead a3 a0 OF ASort  ⇒a0 | AHead  a4⇒a4
                                       <λ:A.A> CASE AHead a1 a2 OF ASort  ⇒a0 | AHead  a4⇒a4

                                     eq
                                       A
                                       λe:A.<λ:A.A> CASE e OF ASort  ⇒a0 | AHead  a4⇒a4 (AHead a3 a0)
                                       λe:A.<λ:A.A> CASE e OF ASort  ⇒a0 | AHead  a4⇒a4 (AHead a1 a2)
                               end of H7
                               suppose : eq A a3 a1
                                  (H11) 
                                     we proceed by induction on H4 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                        case refl_equal : ⇒
                                           the thesis becomes <λ:nat.Prop> CASE S i OF O⇒False | S ⇒True
                                              consider I
                                              we proved True
<λ:nat.Prop> CASE S i OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  end of H11
                                  consider H11
                                  we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  that is equivalent to False
                                  we proceed by induction on the previous result to prove eq A a a1
                                  we proved eq A a a1
(eq A a3 a1)→(eq A a a1)
                            end of h1
                            (h2) 
                               consider H6
                               we proved 
                                  eq
                                    A
                                    <λ:A.A> CASE AHead a3 a0 OF ASort  ⇒a3 | AHead a4 ⇒a4
                                    <λ:A.A> CASE AHead a1 a2 OF ASort  ⇒a3 | AHead a4 ⇒a4
eq A a3 a1
                            end of h2
                            by (h1 h2)
                            we proved eq A a a1
∀H4:(eq nat (S i) O).∀H5:(eq A (AHead a3 a0) (AHead a1 a2)).(eq A a a1)
                we proved (eq nat y0 O)→(eq A y (AHead a1 a2))→(eq A x a1)
             we proved 
                ∀y0:nat
                  .aprem y0 y x
                    →(eq nat y0 O)→(eq A y (AHead a1 a2))→(eq A x a1)
             by (insert_eq . . . . previous H0)
             we proved (eq A y (AHead a1 a2))→(eq A x a1)
          we proved ∀y:A.(aprem O y x)→(eq A y (AHead a1 a2))→(eq A x a1)
          by (insert_eq . . . . previous H)
          we proved eq A x a1
       we proved ∀a1:A.∀a2:A.∀x:A.(aprem O (AHead a1 a2) x)→(eq A x a1)