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