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 =
Show proof