Function to run Intros tactic and give the original proof state back if it fails
Add function to attempt Refine tactic