DEFINITION sc3_cast()
TYPE =
∀g:G
.∀a:A
.∀vs:TList
.∀c:C
.∀u:T
.sc3 g (asucc g a) c (THeads (Flat Appl) vs u)
→∀t:T
.sc3 g a c (THeads (Flat Appl) vs t)
→sc3 g a c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
BODY =
Show proof