DEFINITION sn3_gen_def()
TYPE =
       ∀c:C
         .∀d:C
           .∀v:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) v)
                 →(sn3 c (TLRef i))→(sn3 d v)
BODY =
        assume c: C
        assume d: C
        assume v: T
        assume i: nat
        suppose H: getl i c (CHead d (Bind Abbr) v)
        suppose H0: sn3 c (TLRef i)
          (h1) 
             (h1) 
                by (pr0_refl .)
pr0 (TLRef i) (TLRef i)
             end of h1
             (h2) 
                by (subst0_lref . .)
subst0 i v (TLRef i) (lift (S i) O v)
             end of h2
             by (pr2_delta . . . . H . . h1 . h2)
             we proved pr2 c (TLRef i) (lift (S i) O v)
             by (pr3_pr2 . . . previous)
             we proved pr3 c (TLRef i) (lift (S i) O v)
             by (sn3_pr3_trans . . H0 . previous)
sn3 c (lift (S i) O v)
          end of h1
          (h2) 
             by (getl_drop . . . . . H)
drop (S i) O c d
          end of h2
          by (sn3_gen_lift . . . . h1 . h2)
          we proved sn3 d v
       we proved 
          ∀c:C
            .∀d:C
              .∀v:T
                .∀i:nat
                  .getl i c (CHead d (Bind Abbr) v)
                    →(sn3 c (TLRef i))→(sn3 d v)