-(_: (ty3 g (CHead c (Bind Abst) u) x3 x5)).(and_ind (pc3 c u u) (\forall (b:
-B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x3 t2))) (ex2 T (\lambda (w:
-T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)))
-(\lambda (_: (pc3 c u u)).(\lambda (H10: ((\forall (b: B).(\forall (u0:
-T).(pc3 (CHead c (Bind b) u0) x3 t2))))).(ex_intro2 T (\lambda (w: T).(ty3 g
-c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x4 H6
-(ty3_conv g (CHead c (Bind Abst) u) t2 x0 H3 t1 x3 H7 (H10 Abst u)))))
-(pc3_gen_abst c u u x3 t2 H5))))))))) (ty3_gen_bind g Abst c u t1 (THead
+(_: (ty3 g (CHead c (Bind Abst) u) x3 x5)).(let H_y \def (pc3_gen_abst_shift
+c u x3 t2 H5) in (ex_intro2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_:
+T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x1 H2 (ty3_conv g (CHead c (Bind
+Abst) u) t2 x0 H3 t1 x3 H7 H_y)))))))))) (ty3_gen_bind g Abst c u t1 (THead