DEFINITION arity_sred_pr2()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pr2 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: pr2 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 pr2_free : c0:C t3:T t4:T H0:pr0 t3 t4 ⇒
                the thesis becomes ∀g:G.∀a:A.∀H1:(arity g c0 t3 a).(arity g c0 t4 a)
                    assume g: G
                    assume a: A
                    suppose H1: arity g c0 t3 a
                      by (wcpr0_refl .)
                      we proved wcpr0 c0 c0
                      by (arity_sred_wcpr0_pr0 . . . . H1 . previous . H0)
                      we proved arity g c0 t4 a
∀g:G.∀a:A.∀H1:(arity g c0 t3 a).(arity g c0 t4 a)
             case pr2_delta : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H1:pr0 t3 t4 t:T H2:subst0 i u t4 t ⇒
                the thesis becomes ∀g:G.∀a:A.∀H3:(arity g c0 t3 a).(arity g c0 t a)
                    assume g: G
                    assume a: A
                    suppose H3: arity g c0 t3 a
                      by (wcpr0_refl .)
                      we proved wcpr0 c0 c0
                      by (arity_sred_wcpr0_pr0 . . . . H3 . previous . H1)
                      we proved arity g c0 t4 a
                      by (arity_subst0 . . . . previous . . . H0 . H2)
                      we proved arity g c0 t a
∀g:G.∀a:A.∀H3:(arity g c0 t3 a).(arity g c0 t 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.(pr2 c t1 t2)→∀g:G.∀a:A.(arity g c t1 a)→(arity g c t2 a)