Localy add a theorem template to the def-stobj-preservation-thms database and (nonlocally) prove it about existing functions