DEFINITION sc3_arity_gen()
TYPE =
       ∀g:G.∀c:C.∀t:T.∀a:A.(sc3 g a c t)→(arity g c t a)
BODY =
        assume g: G
        assume c: C
        assume t: T
        assume a: A
          we proceed by induction on a to prove (sc3 g a c t)→(arity g c t a)
             case ASort : n:nat n0:nat ⇒
                the thesis becomes (sc3 g (ASort n n0) c t)→(arity g c t (ASort n n0))
                   we must prove (sc3 g (ASort n n0) c t)→(arity g c t (ASort n n0))
                   or equivalently 
                         land (arity g c t (ASort n n0)) (sn3 c t)
                           →arity g c t (ASort n n0)
                   suppose H: land (arity g c t (ASort n n0)) (sn3 c t)
                      (H0) consider H
                      we proceed by induction on H0 to prove arity g c t (ASort n n0)
                         case conj : H1:arity g c t (ASort n n0) :sn3 c t ⇒
                            the thesis becomes the hypothesis H1
                      we proved arity g c t (ASort n n0)
                   we proved 
                      land (arity g c t (ASort n n0)) (sn3 c t)
                        →arity g c t (ASort n n0)
(sc3 g (ASort n n0) c t)→(arity g c t (ASort n n0))
             case AHead : a0:A a1:A ⇒
                the thesis becomes (sc3 g (AHead a0 a1) c t)→(arity g c t (AHead a0 a1))
                () by induction hypothesis we know (sc3 g a0 c t)→(arity g c t a0)
                () by induction hypothesis we know (sc3 g a1 c t)→(arity g c t a1)
                   we must prove (sc3 g (AHead a0 a1) c t)→(arity g c t (AHead a0 a1))
                   or equivalently 
                         (land
                             arity g c t (AHead a0 a1)
                             ∀d:C
                               .∀w:T
                                 .sc3 g a0 d w
                                   →∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))))
                           →arity g c t (AHead a0 a1)
                   suppose H1: 
                      land
                        arity g c t (AHead a0 a1)
                        ∀d:C
                          .∀w:T
                            .sc3 g a0 d w
                              →∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t)))
                      (H2) consider H1
                      we proceed by induction on H2 to prove arity g c t (AHead a0 a1)
                         case conj : H3:arity g c t (AHead a0 a1) :∀d:C.∀w:T.(sc3 g a0 d w)→∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))) ⇒
                            the thesis becomes the hypothesis H3
                      we proved arity g c t (AHead a0 a1)
                   we proved 
                      (land
                          arity g c t (AHead a0 a1)
                          ∀d:C
                            .∀w:T
                              .sc3 g a0 d w
                                →∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))))
                        →arity g c t (AHead a0 a1)
(sc3 g (AHead a0 a1) c t)→(arity g c t (AHead a0 a1))
          we proved (sc3 g a c t)→(arity g c t a)
       we proved ∀g:G.∀c:C.∀t:T.∀a:A.(sc3 g a c t)→(arity g c t a)