Add a theorem template to the def-stobj-preservation-thms database and prove it about existing functions