misc.workaround_tactics

Global Ltac posed_rewrite t := pose proof t as TEMP; rewrite TEMP; clear TEMP.
Global Ltac apply_simplified x := generalize x; simpl; intro HHH; apply HHH; clear HHH.
Tactic Notation "posed_rewrite" "<-" constr(t) := pose proof t as TEMP; rewrite <-TEMP; clear TEMP.