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