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 =
Show proof