Set Implicit Arguments.
Global Set Asymmetric Patterns.

Ltac hyp := assumption.

Ltac refl := reflexivity.
Ltac reflx := reflexivity.

Ltac gen h := generalize h; clear h.

Ltac ded h := generalize h; intro.

Ltac decomp h := decompose [and or ex] h; clear h.

Ltac discr := intros; discriminate.

Ltac irrefl := intros;
  match goal with
    | _ : ?x = ?x → False |- _ ⇒ absurd (x=x); [assumption | refl]
    | _ : ?x ≠ ?x |- _ ⇒ absurd (x=x); [assumption | refl]
    | _ : ?x ≠ ?y, _ : ?x = ?y |- _ ⇒ subst y; irrefl
    | _ : ?x ≠ ?y, _ : ?y = ?x |- _ ⇒ subst y; irrefl
    | _ : ?x ≠ ?y, _ : ?x = ?z, _ : ?z = ?y |- _ ⇒ subst y; irrefl
    | _ : ?x ≠ ?y, _ : ?x = ?z, _ : ?y = ?z |- _ ⇒ subst y; irrefl
    | _ : ?x ≠ ?y, _ : ?z = ?x, _ : ?z = ?y |- _ ⇒ subst y; irrefl
    | _ : ?x ≠ ?y, _ : ?z = ?x, _ : ?y = ?z |- _ ⇒ subst y; irrefl
  end.

Ltac norm e :=
  let x := fresh in set (x := e); vm_compute in x; subst x.

Ltac norm_in H e :=
  let x := fresh in set (x := e) in H; vm_compute in x; subst x.


Ltac coq_case_eq x := generalize (refl_equal x); pattern x at -1; case x.

Ltac case_eq e := coq_case_eq e; intros.

Section meta.

Lemma contraposee_inv : ∀ P Q : Prop, (P → Q) → ¬Q → ¬P.

Proof.
intros. intro. apply H0. exact (H H1).
Qed.

Variables (A : Type) (P : A → Prop).

Lemma not_exists_imply_forall_not : ~(∃ x, P x) → ∀ x, ¬P x.

Proof.
intros. intro. apply H. ∃ x. exact H0.
Qed.

Lemma forall_not_imply_not_exists : (∀ x, ~(P x)) → ~(∃ x, P x).

Proof.
intros. intro. destruct H0. exact (H x H0).
Qed.

Lemma exists_not_imply_not_forall : (∃ x, ~(P x)) → ~(∀ x, P x).

Proof.
intros. destruct H. intro. ded (H0 x). contradiction.
Qed.

End meta.