DEFINITION ty3_cred_pr3()
TYPE =
       ∀g:G
         .∀c:C
           .∀v1:T
             .∀v2:T
               .pr3 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: pr3 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 pr3_refl : t:T ⇒
                    assume b: B
                    assume t1: T
                    assume t2: T
                    suppose H0: ty3 g (CHead c (Bind b) t) t1 t2
                      consider H0
             case pr3_sing : t2:T t1:T H0:pr2 c t1 t2 t3:T :pr3 c t2 t3 ⇒
                the thesis becomes ∀b:B.∀t0:T.∀t4:T.∀H3:(ty3 g (CHead c (Bind b) t1) t0 t4).(ty3 g (CHead c (Bind b) t3) t0 t4)
                (H2) by induction hypothesis we know ∀b:B.∀t4:T.∀t5:T.(ty3 g (CHead c (Bind b) t2) t4 t5)→(ty3 g (CHead c (Bind b) t3) t4 t5)
                    assume b: B
                    assume t0: T
                    assume t4: T
                    suppose H3: ty3 g (CHead c (Bind b) t1) t0 t4
                      by (ty3_cred_pr2 . . . . H0 . . . H3)
                      we proved ty3 g (CHead c (Bind b) t2) t0 t4
                      by (H2 . . . previous)
                      we proved ty3 g (CHead c (Bind b) t3) t0 t4
∀b:B.∀t0:T.∀t4:T.∀H3:(ty3 g (CHead c (Bind b) t1) t0 t4).(ty3 g (CHead c (Bind b) t3) t0 t4)
          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
                  .pr3 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)