DEFINITION sn3_cast()
TYPE =
       ∀c:C.∀u:T.(sn3 c u)→∀t:T.(sn3 c t)→(sn3 c (THead (Flat Cast) u t))
BODY =
Show proof