Various useful tactics 
version 1.0 
Ltac
elimer e := try exact e; let H := fresh "H" in (generalize e; intro H).
Use a fact, whose type is a nondependent product.
This is modus ponens in forward chaining
use H e when the type of e is A1 > A2 > ... > An > B
will introduce the subgoals Ai and on the last
subgoal will add the hypothesis H : B

Ltac
use H e :=
match type of e with
 ?A > ?B =>
let H' := fresh "H'" in
(assert (H' : A);
[idtac (* we'll return the subgoal A *)
 use H (e H'); try clear H' ])
 ?B => assert (H : B);
[exact e  idtac ]
end.
Like use H H , (use a hypothesis and reuse its name)

Ltac
usehyp H :=
let H' := fresh "H'" in
(use H' H; clear H; try rename H' into H).
This is like rewrite H in *

Ltac
rewriteall H :=
let n := fresh "val" in
(match type of H with
?E1 = ?E2 =>
set (n:= E1) in * ;
clearbody n;
subst n
end).
History 
