DEFINITION thead_x_y_y()
TYPE =
       ∀k:K.∀v:T.∀t:T.(eq T (THead k v t) t)→∀P:Prop.P
BODY =
        assume k: K
        assume v: T
        assume t: T
          we proceed by induction on t to prove (eq T (THead k v t) t)→∀P:Prop.P
             case TSort : n:nat ⇒
                the thesis becomes ∀H:(eq T (THead k v (TSort n)) (TSort n)).∀P:Prop.P
                    suppose H: eq T (THead k v (TSort n)) (TSort n)
                    assume P: Prop
                      (H0) 
                         we proceed by induction on H to prove 
                            <λ:T.Prop>
                              CASE TSort n OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                            case refl_equal : ⇒
                               the thesis becomes 
                               <λ:T.Prop>
                                 CASE THead k v (TSort n) OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                                  consider I
                                  we proved True

                                     <λ:T.Prop>
                                       CASE THead k v (TSort n) OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead   ⇒True

                            <λ:T.Prop>
                              CASE TSort n OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                      end of H0
                      consider H0
                      we proved 
                         <λ:T.Prop>
                           CASE TSort n OF
                             TSort ⇒False
                           | TLRef ⇒False
                           | THead   ⇒True
                      that is equivalent to False
                      we proceed by induction on the previous result to prove P
                      we proved P
∀H:(eq T (THead k v (TSort n)) (TSort n)).∀P:Prop.P
             case TLRef : n:nat ⇒
                the thesis becomes ∀H:(eq T (THead k v (TLRef n)) (TLRef n)).∀P:Prop.P
                    suppose H: eq T (THead k v (TLRef n)) (TLRef n)
                    assume P: Prop
                      (H0) 
                         we proceed by induction on H to prove 
                            <λ:T.Prop>
                              CASE TLRef n OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                            case refl_equal : ⇒
                               the thesis becomes 
                               <λ:T.Prop>
                                 CASE THead k v (TLRef n) OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                                  consider I
                                  we proved True

                                     <λ:T.Prop>
                                       CASE THead k v (TLRef n) OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead   ⇒True

                            <λ:T.Prop>
                              CASE TLRef n OF
                                TSort ⇒False
                              | TLRef ⇒False
                              | THead   ⇒True
                      end of H0
                      consider H0
                      we proved 
                         <λ:T.Prop>
                           CASE TLRef n OF
                             TSort ⇒False
                           | TLRef ⇒False
                           | THead   ⇒True
                      that is equivalent to False
                      we proceed by induction on the previous result to prove P
                      we proved P
∀H:(eq T (THead k v (TLRef n)) (TLRef n)).∀P:Prop.P
             case THead : k0:K t0:T t1:T ⇒
                the thesis becomes ∀H1:(eq T (THead k v (THead k0 t0 t1)) (THead k0 t0 t1)).∀P:Prop.P
                () by induction hypothesis we know (eq T (THead k v t0) t0)→∀P:Prop.P
                (H0) by induction hypothesis we know (eq T (THead k v t1) t1)→∀P:Prop.P
                    suppose H1: eq T (THead k v (THead k0 t0 t1)) (THead k0 t0 t1)
                    assume P: Prop
                      (H2) 
                         by (f_equal . . . . . H1)
                         we proved 
                            eq
                              K
                              <λ:T.K> CASE THead k v (THead k0 t0 t1) OF TSort ⇒k | TLRef ⇒k | THead k1  ⇒k1
                              <λ:T.K> CASE THead k0 t0 t1 OF TSort ⇒k | TLRef ⇒k | THead k1  ⇒k1

                            eq
                              K
                              λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1  ⇒k1
                                THead k v (THead k0 t0 t1)
                              λe:T.<λ:T.K> CASE e OF TSort ⇒k | TLRef ⇒k | THead k1  ⇒k1 (THead k0 t0 t1)
                      end of H2
                      (h1) 
                         (H3) 
                            by (f_equal . . . . . H1)
                            we proved 
                               eq
                                 T
                                 <λ:T.T> CASE THead k v (THead k0 t0 t1) OF TSort ⇒v | TLRef ⇒v | THead  t2 ⇒t2
                                 <λ:T.T> CASE THead k0 t0 t1 OF TSort ⇒v | TLRef ⇒v | THead  t2 ⇒t2

                               eq
                                 T
                                 λe:T.<λ:T.T> CASE e OF TSort ⇒v | TLRef ⇒v | THead  t2 ⇒t2
                                   THead k v (THead k0 t0 t1)
                                 λe:T.<λ:T.T> CASE e OF TSort ⇒v | TLRef ⇒v | THead  t2 ⇒t2 (THead k0 t0 t1)
                         end of H3
                         (h1) 
                            (H4) 
                               by (f_equal . . . . . H1)
                               we proved 
                                  eq
                                    T
                                    <λ:T.T>
                                      CASE THead k v (THead k0 t0 t1) OF
                                        TSort ⇒THead k0 t0 t1
                                      | TLRef ⇒THead k0 t0 t1
                                      | THead   t2⇒t2
                                    <λ:T.T>
                                      CASE THead k0 t0 t1 OF
                                        TSort ⇒THead k0 t0 t1
                                      | TLRef ⇒THead k0 t0 t1
                                      | THead   t2⇒t2

                                  eq
                                    T
                                    λe:T.<λ:T.T> CASE e OF TSort ⇒THead k0 t0 t1 | TLRef ⇒THead k0 t0 t1 | THead   t2⇒t2
                                      THead k v (THead k0 t0 t1)
                                    λe:T.<λ:T.T> CASE e OF TSort ⇒THead k0 t0 t1 | TLRef ⇒THead k0 t0 t1 | THead   t2⇒t2
                                      THead k0 t0 t1
                            end of H4
                             suppose H5: eq T v t0
                             suppose H6: eq K k k0
                               (H7) 
                                  we proceed by induction on H5 to prove (eq T (THead k t0 t1) t1)→∀P0:Prop.P0
                                     case refl_equal : ⇒
                                        the thesis becomes the hypothesis H0
(eq T (THead k t0 t1) t1)→∀P0:Prop.P0
                               end of H7
                               (H8) 
                                  we proceed by induction on H6 to prove (eq T (THead k0 t0 t1) t1)→∀P0:Prop.P0
                                     case refl_equal : ⇒
                                        the thesis becomes the hypothesis H7
(eq T (THead k0 t0 t1) t1)→∀P0:Prop.P0
                               end of H8
                               consider H4
                               we proved 
                                  eq
                                    T
                                    <λ:T.T>
                                      CASE THead k v (THead k0 t0 t1) OF
                                        TSort ⇒THead k0 t0 t1
                                      | TLRef ⇒THead k0 t0 t1
                                      | THead   t2⇒t2
                                    <λ:T.T>
                                      CASE THead k0 t0 t1 OF
                                        TSort ⇒THead k0 t0 t1
                                      | TLRef ⇒THead k0 t0 t1
                                      | THead   t2⇒t2
                               that is equivalent to eq T (THead k0 t0 t1) t1
                               by (H8 previous .)
                               we proved P
(eq T v t0)→(eq K k k0)→P
                         end of h1
                         (h2) 
                            consider H3
                            we proved 
                               eq
                                 T
                                 <λ:T.T> CASE THead k v (THead k0 t0 t1) OF TSort ⇒v | TLRef ⇒v | THead  t2 ⇒t2
                                 <λ:T.T> CASE THead k0 t0 t1 OF TSort ⇒v | TLRef ⇒v | THead  t2 ⇒t2
eq T v t0
                         end of h2
                         by (h1 h2)
(eq K k k0)→P
                      end of h1
                      (h2) 
                         consider H2
                         we proved 
                            eq
                              K
                              <λ:T.K> CASE THead k v (THead k0 t0 t1) OF TSort ⇒k | TLRef ⇒k | THead k1  ⇒k1
                              <λ:T.K> CASE THead k0 t0 t1 OF TSort ⇒k | TLRef ⇒k | THead k1  ⇒k1
eq K k k0
                      end of h2
                      by (h1 h2)
                      we proved P
∀H1:(eq T (THead k v (THead k0 t0 t1)) (THead k0 t0 t1)).∀P:Prop.P
          we proved (eq T (THead k v t) t)→∀P:Prop.P
       we proved ∀k:K.∀v:T.∀t:T.(eq T (THead k v t) t)→∀P:Prop.P