DEFINITION sn3_pr3_trans()
TYPE =
       ∀c:C.∀t1:T.(sn3 c t1)→∀t2:T.(pr3 c t1 t2)→(sn3 c t2)
BODY =
Show proof