DEFINITION ty3_acyclic()
TYPE =
       ∀g:G.∀c:C.∀t:T.∀u:T.(ty3 g c t u)→(pc3 c u t)→∀P:Prop.P
BODY =
        assume g: G
        assume c: C
        assume t: T
        assume u: T
        suppose H: ty3 g c t u
        suppose H0: pc3 c u t
        assume P: Prop
          (H_y) 
             by (ty3_conv . . . . H . . H H0)
ty3 g c t t
          end of H_y
          (H_x) 
             by (ty3_arity . . . . H_y)
ex2 A λa1:A.arity g c t a1 λa1:A.arity g c t (asucc g a1)
          end of H_x
          (H1) consider H_x
          we proceed by induction on H1 to prove P
             case ex_intro2 : x:A H2:arity g c t x H3:arity g c t (asucc g x) ⇒
                the thesis becomes P
                   by (arity_mono . . . . H3 . H2)
                   we proved leq g (asucc g x) x
                   by (leq_asucc_false . . previous .)
P
          we proved P
       we proved ∀g:G.∀c:C.∀t:T.∀u:T.(ty3 g c t u)→(pc3 c u t)→∀P:Prop.P