DEFINITION pc3_gen_not_abst()
TYPE =
       ∀b:B
         .not (eq B b Abst)
           →∀c:C
                .∀t1:T
                  .∀t2:T
                    .∀u1:T
                      .∀u2:T
                        .pc3 c (THead (Bind b) u1 t1) (THead (Bind Abst) u2 t2)
                          →pc3 (CHead c (Bind b) u1) t1 (lift (S O) O (THead (Bind Abst) u2 t2))
BODY =
Show proof