prove proves_cons_def

i.e. it's safe to add a definition to the context of an already proved
theorem, provided the new context is ok.