DEFINITION ty3_cred_pr2()
TYPE =
       ∀g:G
         .∀c:C
           .∀v1:T
             .∀v2:T
               .pr2 c v1 v2
                 →∀b:B.∀t1:T.∀t2:T.(ty3 g (CHead c (Bind b) v1) t1 t2)→(ty3 g (CHead c (Bind b) v2) t1 t2)
BODY =
        assume g: G
        assume c: C
        assume v1: T
        assume v2: T
        suppose H: pr2 c v1 v2
          we proceed by induction on H to prove ∀b:B.∀t1:T.∀t2:T.(ty3 g (CHead c (Bind b) v1) t1 t2)→(ty3 g (CHead c (Bind b) v2) t1 t2)
             case pr2_free : c0:C t1:T t2:T H0:pr0 t1 t2 ⇒
                the thesis becomes ∀b:B.∀t0:T.∀t3:T.∀H1:(ty3 g (CHead c0 (Bind b) t1) t0 t3).(ty3 g (CHead c0 (Bind b) t2) t0 t3)
                    assume b: B
                    assume t0: T
                    assume t3: T
                    suppose H1: ty3 g (CHead c0 (Bind b) t1) t0 t3
                      (h1) 
                         by (wcpr0_refl .)
                         we proved wcpr0 c0 c0
                         by (wcpr0_comp . . previous . . H0 .)
wcpr0 (CHead c0 (Bind b) t1) (CHead c0 (Bind b) t2)
                      end of h1
                      (h2) by (pr0_refl .) we proved pr0 t0 t0
                      by (ty3_sred_wcpr0_pr0 . . . . H1 . h1 . h2)
                      we proved ty3 g (CHead c0 (Bind b) t2) t0 t3
∀b:B.∀t0:T.∀t3:T.∀H1:(ty3 g (CHead c0 (Bind b) t1) t0 t3).(ty3 g (CHead c0 (Bind b) t2) t0 t3)
             case pr2_delta : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) t1:T t2:T H1:pr0 t1 t2 t:T H2:subst0 i u t2 t ⇒
                the thesis becomes ∀b:B.∀t0:T.∀t3:T.∀H3:(ty3 g (CHead c0 (Bind b) t1) t0 t3).(ty3 g (CHead c0 (Bind b) t) t0 t3)
                    assume b: B
                    assume t0: T
                    assume t3: T
                    suppose H3: ty3 g (CHead c0 (Bind b) t1) t0 t3
                      (h1) 
                         (h1) 
                            by (wcpr0_refl .)
                            we proved wcpr0 c0 c0
                            by (wcpr0_comp . . previous . . H1 .)
wcpr0 (CHead c0 (Bind b) t1) (CHead c0 (Bind b) t2)
                         end of h1
                         (h2) by (pr0_refl .) we proved pr0 t0 t0
                         by (ty3_sred_wcpr0_pr0 . . . . H3 . h1 . h2)
ty3 g (CHead c0 (Bind b) t2) t0 t3
                      end of h1
                      (h2) 
                         by (clear_bind . . .)
                         we proved clear (CHead c0 (Bind b) t2) (CHead c0 (Bind b) t2)
                         by (getl_clear_bind . . . . previous . . H0)
getl (S i) (CHead c0 (Bind b) t2) (CHead d (Bind Abbr) u)
                      end of h2
                      (h3) 
                         by (csubst0_snd_bind . . . . . H2 .)
csubst0 (S i) u (CHead c0 (Bind b) t2) (CHead c0 (Bind b) t)
                      end of h3
                      by (ty3_csubst0 . . . . h1 . . . h2 . h3)
                      we proved ty3 g (CHead c0 (Bind b) t) t0 t3
∀b:B.∀t0:T.∀t3:T.∀H3:(ty3 g (CHead c0 (Bind b) t1) t0 t3).(ty3 g (CHead c0 (Bind b) t) t0 t3)
          we proved ∀b:B.∀t1:T.∀t2:T.(ty3 g (CHead c (Bind b) v1) t1 t2)→(ty3 g (CHead c (Bind b) v2) t1 t2)
       we proved 
          ∀g:G
            .∀c:C
              .∀v1:T
                .∀v2:T
                  .pr2 c v1 v2
                    →∀b:B.∀t1:T.∀t2:T.(ty3 g (CHead c (Bind b) v1) t1 t2)→(ty3 g (CHead c (Bind b) v2) t1 t2)