Theorem trivial : ∀ A : Prop, A → A.
auto with v62.
Qed.

Theorem and_commutative : ∀ A B : Prop, A ∧ B → B ∧ A.
intros A B H'; elim H'; auto with v62.
Qed.

Theorem or_commutative : ∀ A B : Prop, A ∨ B → B ∨ A.
intros A B H'; elim H'; auto with v62.
Qed.

Theorem mp : ∀ A B : Prop, A → (A → B) → B.
auto with v62.
Qed.

Theorem S : ∀ A B C : Prop, (A → B → C) → (A → B) → A → C.
auto with v62.
Qed.

Theorem Praeclarum :
 ∀ x y z t : Prop, (x → z) ∧ (y → t) → x ∧ y → z ∧ t.
intros x y z t H'; elim H'.
intros H'0 H'1 H'2; elim H'2.
auto with v62.
Qed.

Theorem resolution :
 ∀ (p q : Type → Prop) (a : Type),
 p a → (∀ x : Type, p x → q x) → q a.
auto with v62.
Qed.

Theorem Witnesses :
 ∀ (a b : Type) (p : Type → Prop), p a ∨ p b → ∃ x : Type, p x.
intros a b p h; elim h;
 [ intro H'; clear h; try exact H' | clear h; intro H' ].
∃ a; try assumption.
∃ b; try assumption.
Qed.

Theorem Simple :
 ∀ (A : Set) (R : A → A → Prop),
 (∀ x y z : A, R x y ∧ R y z → R x z) →
 (∀ x y : A, R x y → R y x) →
 ∀ x : A, (∃ y : A, R x y) → R x x.
intros A R H' H'0 x H'1; try assumption.
elim H'1; intros y E; clear H'1; try exact E.
apply H' with y; auto with v62.
Qed.

Theorem not_not : ∀ a : Prop, a → ¬ ¬ a.
unfold not in |- *; auto with v62.
Qed.

Theorem mini_cases : ∀ x y : Prop, (x ∨ ¬ y) ∧ y → x.
intros x y h; elim h; intros h0 H'; elim h0;
 [ clear h h0; intro H'0 | intro H'0; elim H'0; clear h h0; try assumption ];
 auto with v62.
Qed.

Require Import Classical.

Theorem not_not_converse : ∀ a : Prop, ¬ ¬ a → a.
intros a H'; try assumption; auto 10 with v62.
generalize (classic a); intro h; elim h;
 [ intro H'0; clear h; try exact H'0 | clear h; intro H'0 ].
elim H'; assumption.
Qed.

Theorem not_quite_classic : ∀ a : Prop, ¬ ¬ (a ∨ ¬ a).
unfold not in |- *; auto with v62.
Qed.

Theorem Peirce : ∀ A B : Prop, ((((A → B) → A) → A) → B) → B.
auto with v62.
Qed.