Load param.

Ltac changeall v f P :=
match P with
| v => f
| forall x : ?T, ?b => let T2 := changeall v f T with b2 := changeall v f b in
  constr:(forall x : T2, b2)
| exists x : ?T, ?b => let T2 := changeall v f T with b2 := changeall v f b in
  constr:(exists x : T2, b2)
| (fun x : ?T => ?b) => let T2 := changeall v f T with b2 := changeall v f b in
  constr:(fun x : T2 => b2)
| (?a ?b) => let a2 := changeall v f a with b2 := changeall v f b in
  constr:(a2 b2)
| (?a -> ?b) => let a2 := changeall v f a with b2 := changeall v f b in
  constr:(a2 -> b2)
| _ => P
end.

Ltac setvar v f H :=
match goal with
| [|- ?P] =>
  let P2 := changeall f v P in
  cut (forall v, f = v -> P2) ;
  [intro H ; apply (H (f) (refl_equal _)) | intros v H ]
end.

Ltac var1 v f :=
 let H := fresh "H" in
 setvar v f H
.

Ltac var0 f :=
 let v := fresh "v" in
 let H := fresh "H" in
 setvar v f H
.

Ltac var f :=
 let v := fresh "v" in
 let H := fresh "H" in
 setvar v f H ; (rewrite H || idtac)
.

Ltac genclear H := generalize H ; clear H.

Ltac econtr := eapply False_rect ; eauto.

Ltac invall :=
match goal with
| [ |- ?Q ] =>
 match type of Q with
  | Prop => match goal with
    | [ H : _ /\ _ |- _ ] => inversion_clear H ; invall
    | [ H : exists x, _ |- _ ] => inversion_clear H ; invall
    | [ H : _ <-> _ |- _ ] => inversion_clear H ; invall
    end
 | _ =>
  match goal with
  | [ H : { x : _ & _ } |- _ ] => inversion_clear H ; invall
  | [ H : { x : _ | _ } |- _ ] => inversion_clear H ; invall
  | _ => idtac
  end
 end
end.

Ltac discr :=
match goal with
| [ H1 : ?k = _ , H2 : ?k = _ |- _ ] => rewrite H2 in H1 ; clear H2 ; discr
| [ H1 : ?k = _ , H2 : _ = ?k |- _ ] => rewrite <- H2 in H1 ; clear H2 ; discr
| _ => discriminate
end.


Goal forall (A : Set) (a b c : A) (H1 : a = b) (H2 : a = c), True.
intros.
discr || eauto.
Save.

Goal forall a, a = true -> a = false -> False.
intros.
discr.
Save.

Ltac contreq :=
match goal with
| [ H1 : ?a <> ?a |- _ ] => contradiction (refl_equal a)
| [ H1 : ?a <> ?b , H2 : ?b = ?c |- _ ] => rewrite H2 in H1 ; clear H2 ; contreq
| [ H1 : ?a <> ?b , H2 : ?c = ?b |- _ ] => rewrite <- H2 in H1 ; clear H2 ; contreq
| [ H1 : ?a = ?b -> False, H2 : ?b = ?c |- _ ] => rewrite H2 in H1 ; clear H2 ; contreq
| [ H1 : ?a = ?a -> False |- _  ] => contradiction (refl_equal a)
| [ H1 : ?a = ?b -> False, H2 : ?c = ?b |- _ ] => rewrite <- H2 in H1 ; clear H2 ; contreq
end.

Goal forall (A : Set) (a : A), (a <> a) -> False.
intros.
contreq.
Save.

Ltac introvars :=
match goal with
| [ |- ?P -> ?Q ] => idtac
| [ |- forall _, _ ] => intro ; introvars
| _ => idtac
end.

Goal forall (x y : Type), x = y -> True.
introvars.
auto.
Save.

Ltac dup H := generalize H; intro.

Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
Extract Inductive sigT => "pi" [ "" ].
Extract Inductive prod => "pi" [ "" ].
(* Extract Inductive sig => "" [ "" ]. *)
Extract Inductive sumor => "option" [ "Some" "None" ].


Lemma ex_set_prop : forall (A : Type) P,
{a : A | P a} -> exists a, P a.
Proof.
intros ? ? [a Ha]; exists a; auto.
Qed.

Lemma option_inj : forall A (a : A) b, Some a = Some b -> a = b.
injection 1; auto.
Qed.