(\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) t1 t2))) (pc3
(CHead c (Bind Abst) u) t1 t2) (\lambda (_: (pc3 c u u)).(\lambda (H2:
((\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) t1 t2))))).(H2
(\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) t1 t2))) (pc3
(CHead c (Bind Abst) u) t1 t2) (\lambda (_: (pc3 c u u)).(\lambda (H2:
((\forall (b: B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) t1 t2))))).(H2