(Flat Cast) t t0) t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Flat
Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
(Flat Cast) t t0) t2)) t0 (\lambda (H1: (eq T (THead (Flat Cast) t t0)
(Flat Cast) t t0) t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Flat
Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
(Flat Cast) t t0) t2)) t0 (\lambda (H1: (eq T (THead (Flat Cast) t t0)