DEFINITION arity_sred_wcpr0_pr1()
TYPE =
       ∀t1:T.∀t2:T.(pr1 t1 t2)→∀g:G.∀c1:C.∀a:A.(arity g c1 t1 a)→∀c2:C.(wcpr0 c1 c2)→(arity g c2 t2 a)
BODY =
        assume t1: T
        assume t2: T
        suppose H: pr1 t1 t2
          we proceed by induction on H to prove ∀g:G.∀c1:C.∀a:A.(arity g c1 t1 a)→∀c2:C.(wcpr0 c1 c2)→(arity g c2 t2 a)
             case pr1_refl : t:T ⇒
                the thesis becomes ∀g:G.∀c1:C.∀a:A.∀H0:(arity g c1 t a).∀c2:C.∀H1:(wcpr0 c1 c2).(arity g c2 t a)
                    assume g: G
                    assume c1: C
                    assume a: A
                    suppose H0: arity g c1 t a
                    assume c2: C
                    suppose H1: wcpr0 c1 c2
                      by (pr0_refl .)
                      we proved pr0 t t
                      by (arity_sred_wcpr0_pr0 . . . . H0 . H1 . previous)
                      we proved arity g c2 t a
∀g:G.∀c1:C.∀a:A.∀H0:(arity g c1 t a).∀c2:C.∀H1:(wcpr0 c1 c2).(arity g c2 t a)
             case pr1_sing : t3:T t4:T H0:pr0 t4 t3 t5:T :pr1 t3 t5 ⇒
                the thesis becomes ∀g:G.∀c1:C.∀a:A.∀H3:(arity g c1 t4 a).∀c2:C.∀H4:(wcpr0 c1 c2).(arity g c2 t5 a)
                (H2) by induction hypothesis we know ∀g:G.∀c1:C.∀a:A.(arity g c1 t3 a)→∀c2:C.(wcpr0 c1 c2)→(arity g c2 t5 a)
                    assume g: G
                    assume c1: C
                    assume a: A
                    suppose H3: arity g c1 t4 a
                    assume c2: C
                    suppose H4: wcpr0 c1 c2
                      (h1) 
                         by (arity_sred_wcpr0_pr0 . . . . H3 . H4 . H0)
arity g c2 t3 a
                      end of h1
                      (h2) by (wcpr0_refl .) we proved wcpr0 c2 c2
                      by (H2 . . . h1 . h2)
                      we proved arity g c2 t5 a
∀g:G.∀c1:C.∀a:A.∀H3:(arity g c1 t4 a).∀c2:C.∀H4:(wcpr0 c1 c2).(arity g c2 t5 a)
          we proved ∀g:G.∀c1:C.∀a:A.(arity g c1 t1 a)→∀c2:C.(wcpr0 c1 c2)→(arity g c2 t2 a)
       we proved ∀t1:T.∀t2:T.(pr1 t1 t2)→∀g:G.∀c1:C.∀a:A.(arity g c1 t1 a)→∀c2:C.(wcpr0 c1 c2)→(arity g c2 t2 a)