DEFINITION sn3_cdelta()
TYPE =
       ∀v:T
         .∀t:T
           .∀i:nat
             .∀w:T.(ex T λu:T.subst0 i w t u)
               →∀c:C.∀d:C.(getl i c (CHead d (Bind Abbr) v))→(sn3 c t)→(sn3 d v)
BODY =
Show proof