DEFINITION arity_sred_pr3()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→∀g:G.∀a:A.(arity g c t1 a)→(arity g c t2 a)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr3 c t1 t2
          we proceed by induction on H to prove ∀g:G.∀a:A.(arity g c t1 a)→(arity g c t2 a)
             case pr3_refl : t:T ⇒
                    assume g: G
                    assume a: A
                    suppose H0: arity g c t a
                      consider H0
             case pr3_sing : t3:T t4:T H0:pr2 c t4 t3 t5:T :pr3 c t3 t5 ⇒
                the thesis becomes ∀g:G.∀a:A.∀H3:(arity g c t4 a).(arity g c t5 a)
                (H2) by induction hypothesis we know ∀g:G.∀a:A.(arity g c t3 a)→(arity g c t5 a)
                    assume g: G
                    assume a: A
                    suppose H3: arity g c t4 a
                      by (arity_sred_pr2 . . . H0 . . H3)
                      we proved arity g c t3 a
                      by (H2 . . previous)
                      we proved arity g c t5 a
∀g:G.∀a:A.∀H3:(arity g c t4 a).(arity g c t5 a)
          we proved ∀g:G.∀a:A.(arity g c t1 a)→(arity g c t2 a)
       we proved ∀c:C.∀t1:T.∀t2:T.(pr3 c t1 t2)→∀g:G.∀a:A.(arity g c t1 a)→(arity g c t2 a)