DEFINITION pc3_gen_abst_shift()
TYPE =
       ∀c:C
         .∀u:T
           .∀t1:T
             .∀t2:T
               .pc3 c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)
                 →pc3 (CHead c (Bind Abst) u) t1 t2
BODY =
Show proof