(* from Bart Jacobs (Leuven), The Essence of Coq as a Formal System*)
(* based on a proof by Paolo Capriotti *)
(* to make coq accept it, use the -type-in-type option *)
(* otherwise coq will qualm about the def of spec *)
(* to see why Display universe levels *)

Inductive And(P Q: Type) := and_(p: P)(q: Q).
Inductive Exists(T: Type)(P: T -> Type) := exists_(t: T)(p: P t). 
Inductive Equals(A: Type)(a: A): A -> Type := equals_: Equals A a a.
Inductive False :=.
Definition Not(P: Type) := P -> False.

Inductive U := set(J: Type)(P: J -> Type)(f: J -> U).

Definition In(x X: U): Type := 
match X with
  set J P f => Exists J (fun i => And (P i) (Equals U (f i) x)) 
end.

Definition id(x: U): U := x.
Definition spec(P: U -> Type): U := set U P id.

Definition spec_intro(P: U -> Type)(x: U)(H: P x): In x (spec P) := 
exists_ U (fun (i: U) => And (P i) (Equals U (id i) x))
x (and_ (P x) (Equals U (id x) x) H (equals_ U (id x))).
Definition spec_elim(P: U -> Type)(x: U)(H: In x (spec P)): P x :=
match H with exists_ _ _ i H0 =>
match H0 with and_ _ _ H1 H2 =>
match H2 in Equals _ _ X return P X with equals_ _ _ => H1
end end end.

Definition PR(x: U): Type := Not (In x x).
Definition R: U := spec PR.
Check (spec_intro PR). (* P -> Not P, for P = In R R *)
Check (spec_elim PR R). (* Not P -> P, for P = In R R *)
Definition contradiction(P: Type)(H1: Not P -> P)(H2: P -> Not P): False := 
  (fun (H3: Not P) => H3 (H1 H3)) (fun (HP: P) => H2 HP HP).
Definition absurd: False := 
  contradiction (In R R) (spec_intro PR R) (spec_elim PR R).

Theorem omnipotence : 4 = 3.
Proof.
  apply False_ind.
  apply absurd.
Qed.