Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction