3 Tactic Definition XAuto := Auto with ltlc.
5 Tactic Definition XEAuto := EAuto with ltlc.
7 Tactic Definition XDEAuto d := EAuto d with ltlc.
9 Tactic Definition XElimUsing e v :=
10 Try Intros until v; Elim v using e; Try Clear v.
12 Tactic Definition XElim v := Try Intros until v; Elim v; Try Clear v.
14 Tactic Definition XCase v := Try Intros until v; Case v; Try Clear v.
16 Tactic Definition XReplaceIn Z0 y1 y2 :=
17 Cut y1=y2; [ Intros Z; Rewrite Z in Z0; Clear Z | XAuto ].
19 Theorem insert_eq: (S:Set; x:S; P:S->Prop; G:Prop)
20 ((y:S) (P y) -> y = x -> G) -> (P x) -> G.
23 Tactic Definition InsertEq H y :=
24 Pattern 1 y in H; Match Context With [ _: (?1 y) |- ? ] ->
25 Apply insert_eq with x:=y P:=?1;
26 [ Clear H; Intros until 1 | Pattern y; Apply H ].
28 Theorem unintro : (A:Set; a:A; P:A->Prop) ((x:A) (P x)) -> (P a).
32 Tactic Definition UnIntro Last H :=
34 Match Context With [ y: ?1 |- ?2 ] ->
35 Apply (unintro ?1 y); Clear y.
37 Tactic Definition NonLinear :=
39 [ H: ?1 |- ? ] -> Cut ?1; [ Intros | XAuto ].
41 Tactic Definition XRewrite x :=
43 | [ H0: x = ? |- ? ] -> Try Rewrite H0
44 | [ H0: ? = x |- ? ] -> Try Rewrite <- H0