DEFINITION pr3_gen_cast()
TYPE =
       ∀c:C
         .∀u1:T
           .∀t1:T
             .∀x:T
               .pr3 c (THead (Flat Cast) u1 t1) x
                 →or (ex3_2 T T λu2:T.λt2:T.eq T x (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr3 c u1 u2 λ:T.λt2:T.pr3 c t1 t2) (pr3 c t1 x)
BODY =
Show proof