Added pure logics (logics that only reason about the stack but not the
heap, open Prop to be more precise) as well as a mean to existentialise
program variables, i.e. pull their values to the Coq context.