Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax