T x0) P)))))) (pr3_thin_dx c x0 t2 H7 x f) x t2 (refl_equal T (THead (Flat f)
x t2))) in (land_ind (sn3 c x) (sn3 c t2) (sn3 c t2) (\lambda (_: (sn3 c
x)).(\lambda (H10: (sn3 c t2)).H10)) H8))))))))))))))) y H0))))) H))))).
T x0) P)))))) (pr3_thin_dx c x0 t2 H7 x f) x t2 (refl_equal T (THead (Flat f)
x t2))) in (land_ind (sn3 c x) (sn3 c t2) (sn3 c t2) (\lambda (_: (sn3 c
x)).(\lambda (H10: (sn3 c t2)).H10)) H8))))))))))))))) y H0))))) H))))).