Define a new tactic: existT_eq
Clean up by using existT_eq