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 =
        assume c: C
        assume u: T
        assume t1: T
        assume t2: T
        suppose H: pc3 c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)
          (H_x) 
             by (pc3_gen_abst . . . . . H)
land (pc3 c u u) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
          end of H_x
          (H0) consider H_x
          we proceed by induction on H0 to prove pc3 (CHead c (Bind Abst) u) t1 t2
             case conj : :pc3 c u u H2:∀b:B.∀u0:T.(pc3 (CHead c (Bind b) u0) t1 t2) ⇒
                the thesis becomes pc3 (CHead c (Bind Abst) u) t1 t2
                   by (H2 . .)
pc3 (CHead c (Bind Abst) u) t1 t2
          we proved pc3 (CHead c (Bind Abst) u) t1 t2
       we proved 
          ∀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