Summary: Computer aided proof generation is used for many reasons from formalization of mathematics to formal computer program development. Our research concentrates on completely declarative style proofs used to develop imperative programs in a refinement-based model (i.e. deriving the algorithm from the specification). We investigate why and how to use meta programming techniques for proof development. We examine techniques already used in programming languages if they are applicable for proof construction and point out the specialities caused by the different application area. It is also shown that while meta programming techniques are often dangerous when used to develop programs, they are safe tools for proof development.