DEFINITION ahead_inj_snd()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.∀a3:A.∀a4:A.(leq g (AHead a1 a2) (AHead a3 a4))→(leq g a2 a4)
BODY =
        assume g: G
        assume a1: A
        assume a2: A
        assume a3: A
        assume a4: A
        suppose H: leq g (AHead a1 a2) (AHead a3 a4)
          (H_x) 
             by (leq_gen_head1 . . . . H)
ex3_2 A A λa3:A.λ:A.leq g a1 a3 λ:A.λa4:A.leq g a2 a4 λa3:A.λa4:A.eq A (AHead a3 a4) (AHead a3 a4)
          end of H_x
          (H0) consider H_x
          we proceed by induction on H0 to prove leq g a2 a4
             case ex3_2_intro : x0:A x1:A H1:leq g a1 x0 H2:leq g a2 x1 H3:eq A (AHead a3 a4) (AHead x0 x1) ⇒
                the thesis becomes leq g a2 a4
                   (H4) 
                      by (f_equal . . . . . H3)
                      we proved 
                         eq
                           A
                           <λ:A.A> CASE AHead a3 a4 OF ASort  ⇒a3 | AHead a ⇒a
                           <λ:A.A> CASE AHead x0 x1 OF ASort  ⇒a3 | AHead a ⇒a

                         eq
                           A
                           λe:A.<λ:A.A> CASE e OF ASort  ⇒a3 | AHead a ⇒a (AHead a3 a4)
                           λe:A.<λ:A.A> CASE e OF ASort  ⇒a3 | AHead a ⇒a (AHead x0 x1)
                   end of H4
                   (h1) 
                      (H5) 
                         by (f_equal . . . . . H3)
                         we proved 
                            eq
                              A
                              <λ:A.A> CASE AHead a3 a4 OF ASort  ⇒a4 | AHead  a⇒a
                              <λ:A.A> CASE AHead x0 x1 OF ASort  ⇒a4 | AHead  a⇒a

                            eq
                              A
                              λe:A.<λ:A.A> CASE e OF ASort  ⇒a4 | AHead  a⇒a (AHead a3 a4)
                              λe:A.<λ:A.A> CASE e OF ASort  ⇒a4 | AHead  a⇒a (AHead x0 x1)
                      end of H5
                      suppose H6: eq A a3 x0
                         (H7) 
                            consider H5
                            we proved 
                               eq
                                 A
                                 <λ:A.A> CASE AHead a3 a4 OF ASort  ⇒a4 | AHead  a⇒a
                                 <λ:A.A> CASE AHead x0 x1 OF ASort  ⇒a4 | AHead  a⇒a
                            that is equivalent to eq A a4 x1
                            by (eq_ind_r . . . H2 . previous)
leq g a2 a4
                         end of H7
                         consider H7
                         we proved leq g a2 a4
(eq A a3 x0)→(leq g a2 a4)
                   end of h1
                   (h2) 
                      consider H4
                      we proved 
                         eq
                           A
                           <λ:A.A> CASE AHead a3 a4 OF ASort  ⇒a3 | AHead a ⇒a
                           <λ:A.A> CASE AHead x0 x1 OF ASort  ⇒a3 | AHead a ⇒a
eq A a3 x0
                   end of h2
                   by (h1 h2)
leq g a2 a4
          we proved leq g a2 a4
       we proved ∀g:G.∀a1:A.∀a2:A.∀a3:A.∀a4:A.(leq g (AHead a1 a2) (AHead a3 a4))→(leq g a2 a4)