(_: (pr3 c t3 t5)).(\lambda (H2: ((\forall (f: F).(\forall (v: T).(pr3 (CHead
c (Flat f) v) t3 t5))))).(\lambda (f: F).(\lambda (v: T).(pr3_sing (CHead c
(Flat f) v) t3 t4 (pr2_cflat c t4 t3 H0 f v) t5 (H2 f v)))))))))) t1 t2 H)))).
(_: (pr3 c t3 t5)).(\lambda (H2: ((\forall (f: F).(\forall (v: T).(pr3 (CHead
c (Flat f) v) t3 t5))))).(\lambda (f: F).(\lambda (v: T).(pr3_sing (CHead c
(Flat f) v) t3 t4 (pr2_cflat c t4 t3 H0 f v) t5 (H2 f v)))))))))) t1 t2 H)))).