An Interactive Assistant System for Proving Program Properties