DEFINITION ty3_sn3()
TYPE =
       ∀g:G.∀c:C.∀t:T.∀u:T.(ty3 g c t u)→(sn3 c t)
BODY =
        assume g: G
        assume c: C
        assume t: T
        assume u: T
        suppose H: ty3 g c t u
          (H_x) 
             by (ty3_arity . . . . H)
ex2 A λa1:A.arity g c t a1 λa1:A.arity g c u (asucc g a1)
          end of H_x
          (H0) consider H_x
          we proceed by induction on H0 to prove sn3 c t
             case ex_intro2 : x:A H1:arity g c t x :arity g c u (asucc g x) ⇒
                the thesis becomes sn3 c t
                   by (sc3_arity . . . . H1)
                   we proved sc3 g x c t
                   by (sc3_sn3 . . . . previous)
sn3 c t
          we proved sn3 c t
       we proved ∀g:G.∀c:C.∀t:T.∀u:T.(ty3 g c t u)→(sn3 c t)