DEFINITION csubt_gen_abbr()
TYPE =
       ∀g:G
         .∀e1:C
           .∀c2:C
             .∀v:T
               .csubt g (CHead e1 (Bind Abbr) v) c2
                 →ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abbr) v) λe2:C.csubt g e1 e2
BODY =
Show proof