-w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s
-(Flat Cast) i) v2 t4 w2)) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i
-v2 t4 w2)))) (\lambda (x0: T).(\lambda (H8: (pr0 x x0)).(\lambda (H9: (subst0
-(s (Flat Cast) i) v2 t4 x0)).(or_intror (pr0 (THead (Flat Cast) u x) t4) (ex2
-T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0
-i v2 t4 w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2))
-(\lambda (w2: T).(subst0 i v2 t4 w2)) x0 (pr0_epsilon x x0 H8 u) H9))))) H7))
-(H1 v1 x (s (Flat Cast) i) H6 v2 H3)) w1 H5)))) H4)) (\lambda (H4: (ex3_2 T T
-(\lambda (u2: T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5))))
-(\lambda (u2: T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_:
-T).(\lambda (t5: T).(subst0 (s (Flat Cast) i) v1 t3 t5))))).(ex3_2_ind T T
-(\lambda (u2: T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5))))
-(\lambda (u2: T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_:
-T).(\lambda (t5: T).(subst0 (s (Flat Cast) i) v1 t3 t5))) (or (pr0 w1 t4)
-(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T w1 (THead (Flat Cast)
-x0 x1))).(\lambda (_: (subst0 i v1 u x0)).(\lambda (H7: (subst0 (s (Flat
-Cast) i) v1 t3 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t: T).(or
-(pr0 t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2
-t4 w2))))) (or_ind (pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda
+w2)) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0 (THead
+(Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x0:
+T).(\lambda (H8: (pr0 x x0)).(\lambda (H9: (subst0 (s (Flat Cast) i) v2 t4
+x0)).(or_intror (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0
+(THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))
+(ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2:
+T).(subst0 i v2 t4 w2)) x0 (pr0_tau x x0 H8 u) H9))))) H7)) (H1 v1 x (s (Flat
+Cast) i) H6 v2 H3)) w1 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u2:
+T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
+T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5:
+T).(subst0 (s (Flat Cast) i) v1 t3 t5))))).(ex3_2_ind T T (\lambda (u2:
+T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
+T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5:
+T).(subst0 (s (Flat Cast) i) v1 t3 t5))) (or (pr0 w1 t4) (ex2 T (\lambda (w2:
+T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x0:
+T).(\lambda (x1: T).(\lambda (H5: (eq T w1 (THead (Flat Cast) x0
+x1))).(\lambda (_: (subst0 i v1 u x0)).(\lambda (H7: (subst0 (s (Flat Cast)
+i) v1 t3 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t: T).(or (pr0
+t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4
+w2))))) (or_ind (pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda