DEFINITION sn3_cpr3_trans()
TYPE =
       c:C.u1:T.u2:T.(pr3 c u1 u2)k:K.t:T.(sn3 (CHead c k u1) t)(sn3 (CHead c k u2) t)
BODY =
Show proof