diff --git a/tests/playground/Makefile b/tests/playground/Makefile
index a88cc770d7..a0e3a67900 100644
--- a/tests/playground/Makefile
+++ b/tests/playground/Makefile
@@ -1,6 +1,6 @@
 ## CONFIG
 
-LEAN_BENCHES = binarytrees deriv expr_const_folding qsort rbmap rbmap_checkpoint_10 rbmap_shared unionfind1 unionfind2
+LEAN_BENCHES = binarytrees deriv expr_const_folding frontend qsort rbmap rbmap_checkpoint_10 rbmap_shared unionfind1 unionfind2
 CROSS_BENCHES = binarytrees deriv expr_const_folding qsort rbmap rbmap_checkpoint_10 rbmap_shared
 
 LEAN_CATS = .lean .no_reuse.lean .no_borrow.lean .no_st.lean
@@ -43,7 +43,7 @@ all: reports report_lean.csv report_cross.csv
 %.lean.out: %.lean.cpp
 	$(LEAN_BIN)/leanc $(LEANC_FLAGS) -o $@ $<
 frontend%lean.out:
-	ln -f $(LEAN_BIN)/lean
+	ln -sf $(LEAN_BIN)/lean $@
 # Binaries x.lean.out and x.gcc.lean.out etc. are produced by the
 # same rules and x.lean source file by copying the latter to
 # x.gcc.lean. This also avoids conflicts between intermediate
@@ -92,7 +92,7 @@ bench:
 bench/%.bench: %.out | bench
 	ulimit -s unlimited && $(TEMCI) short exec $(TEMCI_FLAGS) -d $< "./$< $(BENCH_PARAMS)" --out $@
 
-bench/frontend.%.bench: BENCH_PARAMS = --new-frontend ../../library/init/core.lean
+bench/frontend.%.bench: BENCH_PARAMS = --new-frontend frontend_test.lean
 
 bench/binarytrees.%.bench: BENCH_PARAMS = 21
 
diff --git a/tests/playground/bench.nix b/tests/playground/bench.nix
index c740eea40c..6e0dfbfb8e 100644
--- a/tests/playground/bench.nix
+++ b/tests/playground/bench.nix
@@ -50,7 +50,7 @@ in pkgs.stdenv.mkDerivation rec {
   })}/bin";
   LEAN_NO_BORROW_BIN = "${(lean {}).overrideAttrs (attrs: {
     prePatch = ''
-      substituteInPlace library/init/lean/compiler/ir/default.lean --replace "decls.map Decl.inferBorrow" "decls"
+      substituteInPlace library/init/lean/compiler/ir/default.lean --replace "inferBorrow" "pure"
     '';
     preBuild = ''
       # bootstrap changes
diff --git a/tests/playground/frontend_test.lean b/tests/playground/frontend_test.lean
new file mode 100644
index 0000000000..436c2eaf5c
--- /dev/null
+++ b/tests/playground/frontend_test.lean
@@ -0,0 +1,1840 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+notation, basic datatypes and type classes
+-/
+prelude
+
+notation `Prop` := Sort 0
+notation f ` $ `:1 a:0 := f a
+
+/- Logical operations and relations -/
+
+reserve prefix `¬`:40
+reserve prefix `~`:40
+reserve infixr ` ∧ `:35
+reserve infixr ` /\ `:35
+reserve infixr ` \/ `:30
+reserve infixr ` ∨ `:30
+reserve infix ` <-> `:20
+reserve infix ` ↔ `:20
+reserve infix ` = `:50
+reserve infix ` == `:50
+reserve infix ` != `:50
+reserve infix ` ~= `:50
+reserve infix ` ≅ `:50
+reserve infix ` ≠ `:50
+reserve infix ` ≈ `:50
+reserve infix ` ~ `:50
+reserve infix ` ≡ `:50
+reserve infixl ` ⬝ `:75
+reserve infixr ` ▸ `:75
+reserve infixr ` ▹ `:75
+
+/- types and Type constructors -/
+
+reserve infixr ` ⊕ `:30
+reserve infixr ` × `:35
+
+/- arithmetic operations -/
+
+reserve infixl ` + `:65
+reserve infixl ` - `:65
+reserve infixl ` * `:70
+reserve infixl ` / `:70
+reserve infixl ` % `:70
+reserve infixl ` %ₙ `:70
+reserve prefix `-`:100
+reserve infixr ` ^ `:80
+
+reserve infixr ` ∘ `:90
+
+reserve infix ` <= `:50
+reserve infix ` ≤ `:50
+reserve infix ` < `:50
+reserve infix ` >= `:50
+reserve infix ` ≥ `:50
+reserve infix ` > `:50
+
+/- boolean operations -/
+
+reserve prefix `!`:40
+reserve infixl ` && `:35
+reserve infixl ` || `:30
+
+/- set operations -/
+
+reserve infix ` ∈ `:50
+reserve infix ` ∉ `:50
+reserve infixl ` ∩ `:70
+reserve infixl ` ∪ `:65
+reserve infix ` ⊆ `:50
+reserve infix ` ⊇ `:50
+reserve infix ` ⊂ `:50
+reserve infix ` ⊃ `:50
+reserve infix ` \ `:70
+
+/- other symbols -/
+
+reserve infix ` ∣ `:50
+reserve infixl ` ++ `:65
+reserve infixr ` :: `:67
+
+/- Control -/
+reserve infixr ` <|> `:2
+reserve infixr `; `   :3
+reserve infixr ` >>= `:55
+reserve infixr ` >=> `:55
+reserve infixl ` <*> `:60
+reserve infixl ` <* ` :60
+reserve infixr ` *> ` :60
+reserve infixr ` >>> `:60
+reserve infixr ` <$> `:100
+reserve infixr ` <$ ` :100
+reserve infixr ` $> ` :100
+reserve infixl ` <&> `:100
+
+universes u v w
+
+/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/
+unsafe axiom lcProof {α : Prop} : α
+/-- Auxiliary unsafe constant used by the Compiler to mark unreachable code. -/
+unsafe axiom lcUnreachable {α : Sort u} : α
+
+@[inline] def id {α : Sort u} (a : α) : α := a
+
+def inline {α : Sort u} (a : α) : α := a
+
+@[inline] def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ :=
+λ b a, f a b
+
+/-
+The kernel definitional equality test (t =?= s) has special support for idDelta applications.
+It implements the following rules
+
+   1)   (idDelta t) =?= t
+   2)   t =?= (idDelta t)
+   3)   (idDelta t) =?= s  IF (unfoldOf t) =?= s
+   4)   t =?= idDelta s    IF t =?= (unfoldOf s)
+
+This is mechanism for controlling the delta reduction (aka unfolding) used in the kernel.
+
+We use idDelta applications to address performance problems when Type checking
+theorems generated by the equation Compiler.
+-/
+@[inline] def idDelta {α : Sort u} (a : α) : α :=
+a
+
+/-- Gadget for optional parameter support. -/
+@[reducible] def optParam (α : Sort u) (default : α) : Sort u :=
+α
+
+/-- Gadget for marking output parameters in type classes. -/
+@[reducible] def outParam (α : Sort u) : Sort u := α
+
+/-- Auxiliary Declaration used to implement the notation (a : α) -/
+@[reducible] def typedExpr (α : Sort u) (a : α) : α := a
+
+/- `idRhs` is an auxiliary Declaration used in the equation Compiler to address performance
+   issues when proving equational theorems. The equation Compiler uses it as a marker. -/
+@[macroInline] abbrev idRhs (α : Sort u) (a : α) : α := a
+
+inductive PUnit : Sort u
+| unit : PUnit
+
+/-- An abbreviation for `PUnit.{0}`, its most common instantiation.
+    This Type should be preferred over `PUnit` where possible to avoid
+    unnecessary universe parameters. -/
+abbrev Unit : Type := PUnit
+
+@[pattern] abbrev Unit.unit : Unit := PUnit.unit
+
+/- Remark: thunks have an efficient implementation in the runtime. -/
+structure Thunk (α : Type u) : Type u :=
+(fn : Unit → α)
+
+attribute [extern cpp inline "lean::mk_thunk(#2)"] Thunk.mk
+
+@[noinline, extern cpp inline "lean::thunk_pure(#2)"]
+protected def Thunk.pure {α : Type u} (a : α) : Thunk α :=
+⟨λ _, a⟩
+@[noinline, extern cpp inline "lean::thunk_get_own(#2)"]
+protected def Thunk.get {α : Type u} (x : @& Thunk α) : α :=
+x.fn ()
+@[noinline, extern cpp inline "lean::thunk_map(#3, #4)"]
+protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β :=
+⟨λ _, f x.get⟩
+@[noinline, extern cpp inline "lean::thunk_bind(#3, #4)"]
+protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
+⟨λ _, (f x.get).get⟩
+
+/- Remark: tasks have an efficient implementation in the runtime. -/
+structure Task (α : Type u) : Type u :=
+(fn : Unit → α)
+
+attribute [extern cpp inline "lean::mk_task(#2)"] Task.mk
+
+@[noinline, extern cpp inline "lean::task_pure(#2)"]
+protected def Task.pure {α : Type u} (a : α) : Task α :=
+⟨λ _, a⟩
+@[noinline, extern cpp inline "lean::task_get(#2)"]
+protected def Task.get {α : Type u} (x : @& Task α) : α :=
+x.fn ()
+@[noinline, extern cpp inline "lean::task_map(#3, #4)"]
+protected def Task.map {α : Type u} {β : Type v} (f : α → β) (x : Task α) : Task β :=
+⟨λ _, f x.get⟩
+@[noinline, extern cpp inline "lean::task_bind(#3, #4)"]
+protected def Task.bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) : Task β :=
+⟨λ _, (f x.get).get⟩
+
+inductive True : Prop
+| intro : True
+
+inductive False : Prop
+
+inductive Empty : Type
+
+def Not (a : Prop) : Prop := a → False
+prefix `¬` := Not
+
+inductive Eq {α : Sort u} (a : α) : α → Prop
+| refl : Eq a
+
+@[elabAsEliminator, inline, reducible]
+def {u1 u2} Eq.ndrec {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
+@Eq.rec α a (λ α _, C α) m b h
+
+@[elabAsEliminator, inline, reducible]
+def {u1 u2} Eq.ndrecOn {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
+@Eq.rec α a (λ α _, C α) m b h
+
+/-
+Initialize the Quotient Module, which effectively adds the following definitions:
+
+constant Quot {α : Sort u} (r : α → α → Prop) : Sort u
+
+constant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
+
+constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
+  (∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β
+
+constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
+  (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
+-/
+initQuot
+
+inductive Heq {α : Sort u} (a : α) : Π {β : Sort u}, β → Prop
+| refl : Heq a
+
+structure Prod (α : Type u) (β : Type v) :=
+(fst : α) (snd : β)
+
+/-- Similar to `Prod`, but α and β can be propositions.
+   We use this Type internally to automatically generate the brecOn recursor. -/
+structure PProd (α : Sort u) (β : Sort v) :=
+(fst : α) (snd : β)
+
+structure And (a b : Prop) : Prop :=
+intro :: (left : a) (right : b)
+
+structure Iff (a b : Prop) : Prop :=
+intro :: (mp : a → b) (mpr : b → a)
+
+/- Eq basic support -/
+
+infix = := Eq
+
+@[pattern] def rfl {α : Sort u} {a : α} : a = a := Eq.refl a
+
+@[elabAsEliminator]
+theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
+Eq.ndrec h₂ h₁
+
+infixr ▸ := Eq.subst
+
+theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
+h₂ ▸ h₁
+
+theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
+h ▸ rfl
+
+infix ~= := Heq
+infix ≅ := Heq
+
+@[pattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a
+
+theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
+have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a', from
+  λ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a'), Heq.recOn h₁ (λ h₂ : α = α, rfl),
+show (Eq.ndrecOn (Eq.refl α) a : α) = a', from
+  this α a' h (Eq.refl α)
+
+inductive Sum (α : Type u) (β : Type v)
+| inl {} (val : α) : Sum
+| inr {} (val : β) : Sum
+
+inductive PSum (α : Sort u) (β : Sort v)
+| inl {} (val : α) : PSum
+| inr {} (val : β) : PSum
+
+inductive Or (a b : Prop) : Prop
+| inl {} (h : a) : Or
+| inr {} (h : b) : Or
+
+def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b :=
+Or.inl ha
+
+def Or.introRight (a : Prop) {b : Prop} (hb : b) : Or a b :=
+Or.inr hb
+
+structure Sigma {α : Type u} (β : α → Type v) :=
+mk :: (fst : α) (snd : β fst)
+
+structure PSigma {α : Sort u} (β : α → Sort v) :=
+mk :: (fst : α) (snd : β fst)
+
+inductive Bool : Type
+| false : Bool
+| true : Bool
+
+/- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/
+structure Subtype {α : Sort u} (p : α → Prop) :=
+(val : α) (property : p val)
+
+inductive Exists {α : Sort u} (p : α → Prop) : Prop
+| intro (w : α) (h : p w) : Exists
+
+attribute [ppAsAnonymousCtor] Sigma PSigma Subtype PProd And
+
+class inductive Decidable (p : Prop)
+| isFalse (h : ¬p) : Decidable
+| isTrue  (h : p) : Decidable
+
+@[reducible] def DecidablePred {α : Sort u} (r : α → Prop) :=
+Π (a : α), Decidable (r a)
+
+@[reducible] def DecidableRel {α : Sort u} (r : α → α → Prop) :=
+Π (a b : α), Decidable (r a b)
+
+class DecidableEq (α : Sort u) :=
+{decEq : Π a b : α, Decidable (a = b)}
+
+export DecidableEq (decEq)
+
+@[inline] instance decidableOfDecidableEq {α : Sort u} (a b : α) [DecidableEq α] : Decidable (a = b) :=
+decEq a b
+
+inductive Option (α : Type u)
+| none {} : Option
+| some (val : α) : Option
+
+export Option (none some)
+export Bool (false true)
+
+inductive List (T : Type u)
+| nil {} : List
+| cons (hd : T) (tl : List) : List
+
+infixr :: := List.cons
+notation `[` l:(foldr `, ` (h t, List.cons h t) List.nil `]`) := l
+
+inductive Nat
+| zero : Nat
+| succ (n : Nat) : Nat
+
+/- Auxiliary axiom used to implement `sorry`.
+   TODO: add this theorem on-demand. That is,
+   we should only add it if after the first error. -/
+unsafe axiom sorryAx (α : Sort u) (synthetic := true) : α
+
+/- Declare builtin and reserved notation -/
+
+class HasZero     (α : Type u) := (zero : α)
+class HasOne      (α : Type u) := (one : α)
+class HasAdd      (α : Type u) := (add : α → α → α)
+class HasMul      (α : Type u) := (mul : α → α → α)
+class HasNeg      (α : Type u) := (neg : α → α)
+class HasSub      (α : Type u) := (sub : α → α → α)
+class HasDiv      (α : Type u) := (div : α → α → α)
+class HasDivides  (α : Type u) := (Divides : α → α → Prop)
+class HasMod      (α : Type u) := (mod : α → α → α)
+class HasModn     (α : Type u) := (modn : α → Nat → α)
+class HasLessEq   (α : Type u) := (LessEq : α → α → Prop)
+class HasLess     (α : Type u) := (Less : α → α → Prop)
+class HasBeq      (α : Type u) := (beq : α → α → Bool)
+class HasAppend   (α : Type u) := (append : α → α → α)
+class HasOrelse   (α : Type u) := (orelse  : α → α → α)
+class HasAndthen  (α : Type u) := (andthen : α → α → α)
+class HasUnion    (α : Type u) := (union : α → α → α)
+class HasInter    (α : Type u) := (inter : α → α → α)
+class HasSDiff    (α : Type u) := (sdiff : α → α → α)
+class HasEquiv    (α : Sort u) := (Equiv : α → α → Prop)
+class HasSubset   (α : Type u) := (Subset : α → α → Prop)
+class HasSSubset  (α : Type u) := (SSubset : α → α → Prop)
+/- Type classes HasEmptyc and HasInsert are
+   used to implement polymorphic notation for collections.
+   Example: {a, b, c}. -/
+class HasEmptyc   (α : Type u) := (emptyc : α)
+class HasInsert   (α : outParam $ Type u) (γ : Type v) := (insert : α → γ → γ)
+/- Type class used to implement the notation { a ∈ c | p a } -/
+class HasSep (α : outParam $ Type u) (γ : Type v) :=
+(sep : (α → Prop) → γ → γ)
+/- Type class for set-like membership -/
+class HasMem (α : outParam $ Type u) (γ : Type v) := (mem : α → γ → Prop)
+
+class HasPow (α : Type u) (β : Type v) :=
+(pow : α → β → α)
+
+export HasAndthen (andthen)
+export HasPow (pow)
+
+infix ∈        := HasMem.mem
+notation a ` ∉ ` s := ¬ HasMem.mem a s
+infix +        := HasAdd.add
+infix *        := HasMul.mul
+infix -        := HasSub.sub
+infix /        := HasDiv.div
+infix ∣        := HasDivides.Divides
+infix %        := HasMod.mod
+infix %ₙ       := HasModn.modn
+prefix -       := HasNeg.neg
+infix <=       := HasLessEq.LessEq
+infix ≤        := HasLessEq.LessEq
+infix <        := HasLess.Less
+infix ==       := HasBeq.beq
+infix ++       := HasAppend.append
+notation `∅`   := HasEmptyc.emptyc _
+infix ∪        := HasUnion.union
+infix ∩        := HasInter.inter
+infix ⊆        := HasSubset.Subset
+infix ⊂        := HasSSubset.SSubset
+infix \        := HasSDiff.sdiff
+infix ≈        := HasEquiv.Equiv
+infixr ^       := HasPow.pow
+infixr /\      := And
+infixr ∧       := And
+infixr \/      := Or
+infixr ∨       := Or
+infix <->      := Iff
+infix ↔        := Iff
+notation `exists` binders `, ` r:(scoped P, Exists P) := r
+notation `∃` binders `, ` r:(scoped P, Exists P) := r
+infixr <|>     := HasOrelse.orelse
+infixr ;       := HasAndthen.andthen
+
+export HasAppend (append)
+
+@[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a
+@[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop     := HasLess.Less b a
+
+infix >=       := GreaterEq
+infix ≥        := GreaterEq
+infix >        := Greater
+
+@[reducible] def Superset {α : Type u} [HasSubset α] (a b : α) : Prop := HasSubset.Subset b a
+@[reducible] def SSuperset {α : Type u} [HasSSubset α] (a b : α) : Prop := HasSSubset.SSubset b a
+
+infix ⊇        := Superset
+infix ⊃        := SSuperset
+
+@[inline] def bit0 {α : Type u} [s  : HasAdd α] (a  : α)                 : α := a + a
+@[inline] def bit1 {α : Type u} [s₁ : HasOne α] [s₂ : HasAdd α] (a : α) : α := (bit0 a) + 1
+
+attribute [pattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg
+
+export HasInsert (insert)
+
+/- The Empty collection -/
+@[inline] def singleton {α : Type u} {γ : Type v} [HasEmptyc γ] [HasInsert α γ] (a : α) : γ :=
+HasInsert.insert a ∅
+
+/- Nat basic instances -/
+@[extern cpp "lean::nat_add"]
+protected def Nat.add : (@& Nat) → (@& Nat) → Nat
+| a  Nat.zero     := a
+| a  (Nat.succ b) := Nat.succ (Nat.add a b)
+
+/- We mark the following definitions as pattern to make sure they can be used in recursive equations,
+   and reduced by the equation Compiler. -/
+attribute [pattern] Nat.add Nat.add._main
+
+instance : HasZero Nat := ⟨Nat.zero⟩
+
+instance : HasOne Nat := ⟨Nat.succ (Nat.zero)⟩
+
+instance : HasAdd Nat := ⟨Nat.add⟩
+
+/- Auxiliary constant used by equation compiler. -/
+constant hugeFuel : Nat := 10000
+
+def std.priority.default : Nat := 1000
+def std.priority.max     : Nat := 0xFFFFFFFF
+
+protected def Nat.prio := std.priority.default + 100
+
+/-
+  Global declarations of right binding strength
+
+  If a Module reassigns these, it will be incompatible with other modules that adhere to these
+  conventions.
+
+  When hovering over a symbol, use "C-c C-k" to see how to input it.
+-/
+def std.prec.max   : Nat := 1024 -- the strength of application, identifiers, (, [, etc.
+def std.prec.arrow : Nat := 25
+
+/-
+The next def is "max + 10". It can be used e.g. for postfix operations that should
+be stronger than application.
+-/
+
+def std.prec.maxPlus : Nat := std.prec.max + 10
+
+infixr × := Prod
+-- notation for n-ary tuples
+
+/- Some type that is not a scalar value in our runtime.
+   TODO: mark opaque -/
+structure NonScalar :=
+(val : Nat)
+
+/- sizeof -/
+
+class HasSizeof (α : Sort u) :=
+(sizeof : α → Nat)
+
+export HasSizeof (sizeof)
+
+/-
+Declare sizeof instances and theorems for types declared before HasSizeof.
+From now on, the inductive Compiler will automatically generate sizeof instances and theorems.
+-/
+
+/- Every Type `α` has a default HasSizeof instance that just returns 0 for every element of `α` -/
+protected def default.sizeof (α : Sort u) : α → Nat
+| a := 0
+
+instance defaultHasSizeof (α : Sort u) : HasSizeof α :=
+⟨default.sizeof α⟩
+
+protected def Nat.sizeof : Nat → Nat
+| n := n
+
+instance : HasSizeof Nat :=
+⟨Nat.sizeof⟩
+
+protected def Prod.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Prod α β) → Nat
+| ⟨a, b⟩ := 1 + sizeof a + sizeof b
+
+instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) :=
+⟨Prod.sizeof⟩
+
+protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Sum α β) → Nat
+| (Sum.inl a) := 1 + sizeof a
+| (Sum.inr b) := 1 + sizeof b
+
+instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) :=
+⟨Sum.sizeof⟩
+
+protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat
+| (PSum.inl a) := 1 + sizeof a
+| (PSum.inr b) := 1 + sizeof b
+
+instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) :=
+⟨PSum.sizeof⟩
+
+protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Sigma β → Nat
+| ⟨a, b⟩ := 1 + sizeof a + sizeof b
+
+instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) :=
+⟨Sigma.sizeof⟩
+
+protected def PSigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : PSigma β → Nat
+| ⟨a, b⟩ := 1 + sizeof a + sizeof b
+
+instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (PSigma β) :=
+⟨PSigma.sizeof⟩
+
+protected def PUnit.sizeof : PUnit → Nat
+| u := 1
+
+instance : HasSizeof PUnit := ⟨PUnit.sizeof⟩
+
+protected def Bool.sizeof : Bool → Nat
+| b := 1
+
+instance : HasSizeof Bool := ⟨Bool.sizeof⟩
+
+protected def Option.sizeof {α : Type u} [HasSizeof α] : Option α → Nat
+| none     := 1
+| (some a) := 1 + sizeof a
+
+instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) :=
+⟨Option.sizeof⟩
+
+protected def List.sizeof {α : Type u} [HasSizeof α] : List α → Nat
+| List.nil        := 1
+| (List.cons a l) := 1 + sizeof a + List.sizeof l
+
+instance (α : Type u) [HasSizeof α] : HasSizeof (List α) :=
+⟨List.sizeof⟩
+
+protected def Subtype.sizeof {α : Type u} [HasSizeof α] {p : α → Prop} : Subtype p → Nat
+| ⟨a, _⟩ := sizeof a
+
+instance {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) :=
+⟨Subtype.sizeof⟩
+
+theorem natAddZero (n : Nat) : n + 0 = n := rfl
+
+theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rfl
+
+/-- Like `by applyInstance`, but not dependent on the tactic framework. -/
+@[reducible] def inferInstance {α : Type u} [i : α] : α := i
+@[reducible, elabSimple] def inferInstanceAs (α : Type u) [i : α] : α := i
+
+/- Boolean operators -/
+
+@[macroInline] def cond {a : Type u} : Bool → a → a → a
+| true  x y := x
+| false x y := y
+
+@[macroInline] def or : Bool → Bool → Bool
+| true  _  := true
+| false b  := b
+
+@[macroInline] def and : Bool → Bool → Bool
+| false _  := false
+| true  b  := b
+
+@[macroInline] def not : Bool → Bool
+| true  := false
+| false := true
+
+@[macroInline] def xor : Bool → Bool → Bool
+| true  b := not b
+| false b := b
+
+prefix ! := not
+infix || := or
+infix && := and
+
+@[extern cpp inline "#1 || #2"] def strictOr  (b₁ b₂ : Bool) := b₁ || b₂
+@[extern cpp inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂
+
+@[inline] def bne {α : Type u} [HasBeq α] (a b : α) : Bool :=
+!(a == b)
+
+infix != := bne
+
+/- Logical connectives an equality -/
+
+def implies (a b : Prop) := a → b
+
+theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
+assume hp, h₂ (h₁ hp)
+
+def trivial : True := ⟨⟩
+
+@[macroInline] def False.elim {C : Sort u} (h : False) : C :=
+False.rec (λ _, C) h
+
+@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
+False.elim (h₂ h₁)
+
+theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)
+
+theorem notFalse : ¬False := id
+
+-- proof irrelevance is built in
+theorem proofIrrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
+
+theorem id.def {α : Sort u} (a : α) : id a = a := rfl
+
+@[macroInline] def Eq.mp {α β : Sort u} (h₁ : α = β) (h₂ : α) : β :=
+Eq.recOn h₁ h₂
+
+@[macroInline] def Eq.mpr {α β : Sort u} : (α = β) → β → α :=
+λ h₁ h₂, Eq.recOn (Eq.symm h₁) h₂
+
+@[elabAsEliminator]
+theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
+Eq.subst (Eq.symm h₁) h₂
+
+theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
+Eq.subst h₁ (Eq.subst h₂ rfl)
+
+theorem congrFun {α : Sort u} {β : α → Sort v} {f g : Π x, β x} (h : f = g) (a : α) : f a = g a :=
+Eq.subst h (Eq.refl (f a))
+
+theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂ :=
+congr rfl h
+
+theorem transRelLeft {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
+h₂ ▸ h₁
+
+theorem transRelRight {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
+h₁.symm ▸ h₂
+
+theorem ofEqTrue {p : Prop} (h : p = True) : p :=
+h.symm ▸ trivial
+
+theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
+assume hp, h ▸ hp
+
+@[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β :=
+Eq.rec a h
+
+theorem castProofIrrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl
+
+theorem castEq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl
+
+@[reducible] def Ne {α : Sort u} (a b : α) := ¬(a = b)
+infix ≠ := Ne
+
+theorem Ne.def {α : Sort u} (a b : α) : a ≠ b = ¬ (a = b) := rfl
+
+section Ne
+variable {α : Sort u}
+variables {a b : α} {p : Prop}
+
+theorem Ne.intro (h : a = b → False) : a ≠ b := h
+
+theorem Ne.elim (h : a ≠ b) : a = b → False := h
+
+theorem Ne.irrefl (h : a ≠ a) : False := h rfl
+
+theorem Ne.symm (h : a ≠ b) : b ≠ a :=
+assume (h₁ : b = a), h (h₁.symm)
+
+theorem falseOfNe : a ≠ a → False := Ne.irrefl
+
+theorem neFalseOfSelf : p → p ≠ False :=
+assume (hp : p) (Heq : p = False), Heq ▸ hp
+
+theorem neTrueOfNot : ¬p → p ≠ True :=
+assume (hnp : ¬p) (Heq : p = True), (Heq ▸ hnp) trivial
+
+theorem trueNeFalse : ¬True = False :=
+neFalseOfSelf trivial
+end Ne
+
+theorem eqFalseOfNeTrue : ∀ {b : Bool}, b ≠ true → b = false
+| true h := False.elim (h rfl)
+| false h := rfl
+
+theorem eqTrueOfNeFalse : ∀ {b : Bool}, b ≠ false → b = true
+| true h := rfl
+| false h := False.elim (h rfl)
+
+section
+variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
+
+@[elabAsEliminator]
+theorem {u1 u2} Heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
+@Heq.rec α a (λ β b _, C b) m β b h
+
+@[elabAsEliminator]
+theorem {u1 u2} Heq.ndrecOn {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
+@Heq.rec α a (λ β b _, C b) m β b h
+
+theorem Heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
+Eq.recOn (eqOfHeq h₁) h₂
+
+theorem Heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
+Heq.ndrecOn h₁ h₂
+
+theorem Heq.symm (h : a ≅ b) : b ≅ a :=
+Heq.ndrecOn h (Heq.refl a)
+
+theorem heqOfEq (h : a = a') : a ≅ a' :=
+Eq.subst h (Heq.refl a)
+
+theorem Heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
+Heq.subst h₂ h₁
+
+theorem heqOfHeqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
+Heq.trans h₁ (heqOfEq h₂)
+
+theorem heqOfEqOfHeq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
+Heq.trans (heqOfEq h₁) h₂
+
+def typeEqOfHeq (h : a ≅ b) : α = β :=
+Heq.ndrecOn h (Eq.refl α)
+end
+
+theorem eqRecHeq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
+| a _ rfl p := Heq.refl p
+
+theorem ofHeqTrue {a : Prop} (h : a ≅ True) : a :=
+ofEqTrue (eqOfHeq h)
+
+theorem castHeq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
+| α _ rfl a := Heq.refl a
+
+variables {a b c d : Prop}
+
+theorem And.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c :=
+And.rec h₂ h₁
+
+theorem And.swap : a ∧ b → b ∧ a :=
+assume ⟨ha, hb⟩, ⟨hb, ha⟩
+
+def And.symm := @And.swap
+
+theorem Or.elim (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) : c :=
+Or.rec h₂ h₃ h₁
+
+theorem Or.swap (h : a ∨ b) : b ∨ a :=
+Or.elim h Or.inr Or.inl
+
+def Or.symm := @Or.swap
+
+/- xor -/
+def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
+
+@[recursor 5]
+theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
+Iff.rec h₁ h₂
+
+theorem Iff.left : (a ↔ b) → a → b := Iff.mp
+
+theorem Iff.right : (a ↔ b) → b → a := Iff.mpr
+
+theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
+Iff.intro (λ h, And.intro h.mp h.mpr) (λ h, Iff.intro h.left h.right)
+
+theorem Iff.refl (a : Prop) : a ↔ a :=
+Iff.intro (assume h, h) (assume h, h)
+
+theorem Iff.rfl {a : Prop} : a ↔ a :=
+Iff.refl a
+
+theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
+Iff.intro
+  (assume ha, Iff.mp h₂ (Iff.mp h₁ ha))
+  (assume hc, Iff.mpr h₁ (Iff.mpr h₂ hc))
+
+theorem Iff.symm (h : a ↔ b) : b ↔ a :=
+Iff.intro (Iff.right h) (Iff.left h)
+
+theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
+Iff.intro Iff.symm Iff.symm
+
+theorem Eq.toIff {a b : Prop} (h : a = b) : a ↔ b :=
+Eq.recOn h Iff.rfl
+
+theorem neqOfNotIff {a b : Prop} : ¬(a ↔ b) → a ≠ b :=
+λ h₁ h₂,
+have a ↔ b, from Eq.subst h₂ (Iff.refl a),
+absurd this h₁
+
+theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
+Iff.intro
+ (assume (hna : ¬ a) (hb : b), hna (Iff.right h₁ hb))
+ (assume (hnb : ¬ b) (ha : a), hnb (Iff.left h₁ ha))
+
+theorem ofIffTrue (h : a ↔ True) : a :=
+Iff.mp (Iff.symm h) trivial
+
+theorem notOfIffFalse : (a ↔ False) → ¬a := Iff.mp
+
+theorem iffTrueIntro (h : a) : a ↔ True :=
+Iff.intro
+  (λ hl, trivial)
+  (λ hr, h)
+
+theorem iffFalseIntro (h : ¬a) : a ↔ False :=
+Iff.intro h (False.rec (λ _, a))
+
+theorem notNotIntro (ha : a) : ¬¬a :=
+assume hna : ¬a, hna ha
+
+theorem notTrue : (¬ True) ↔ False :=
+iffFalseIntro (notNotIntro trivial)
+
+/- or resolution rulses -/
+
+theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
+Or.elim h (λ ha, absurd ha na) id
+
+theorem negResolveLeft {a b : Prop} (h : ¬ a ∨ b) (ha : a) : b :=
+Or.elim h (λ na, absurd ha na) id
+
+theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬ b) : a :=
+Or.elim h id (λ hb, absurd hb nb)
+
+theorem negResolveRight {a b : Prop} (h : a ∨ ¬ b) (hb : b) : a :=
+Or.elim h id (λ nb, absurd hb nb)
+
+/- Exists -/
+
+theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
+  (h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b :=
+Exists.rec h₂ h₁
+
+/- Decidable -/
+
+@[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
+Decidable.casesOn h (λ h₁, false) (λ h₂, true)
+
+export Decidable (isTrue isFalse decide)
+
+instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α :=
+⟨λ a b, decide (a = b)⟩
+
+theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
+Decidable.casesOn h (λ h, False.elim (Iff.mp notTrue h)) (λ _, rfl)
+
+theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
+Decidable.casesOn h (λ h, rfl) (λ h, False.elim h)
+
+instance : Decidable True :=
+isTrue trivial
+
+instance : Decidable False :=
+isFalse notFalse
+
+-- We use "dependent" if-then-else to be able to communicate the if-then-else condition
+-- to the branches
+@[macroInline] def dite (c : Prop) [h : Decidable c] {α : Sort u} : (c → α) → (¬ c → α) → α :=
+λ t e, Decidable.casesOn h e t
+
+/- if-then-else -/
+
+@[macroInline] def ite (c : Prop) [h : Decidable c] {α : Sort u} (t e : α) : α :=
+Decidable.casesOn h (λ hnc, e) (λ hc, t)
+
+namespace Decidable
+variables {p q : Prop}
+
+def recOnTrue [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃)
+    : (Decidable.recOn h h₂ h₁ : Sort u) :=
+Decidable.casesOn h (λ h, False.rec _ (h h₃)) (λ h, h₄)
+
+def recOnFalse [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃)
+    : (Decidable.recOn h h₂ h₁ : Sort u) :=
+Decidable.casesOn h (λ h, h₄) (λ h, False.rec _ (h₃ h))
+
+@[macroInline] def byCases {q : Sort u} [s : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q :=
+match s with
+| isTrue h  := h1 h
+| isFalse h := h2 h
+
+theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
+byCases Or.inl Or.inr
+
+theorem byContradiction [Decidable p] (h : ¬p → False) : p :=
+byCases id (λ np : ¬p, False.elim (h np))
+
+theorem ofNotNot [Decidable p] : ¬ ¬ p → p :=
+λ hnn, byContradiction (λ hn, absurd hn hnn)
+
+theorem notNotIff (p) [Decidable p] : (¬ ¬ p) ↔ p :=
+Iff.intro ofNotNot notNotIntro
+
+theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q :=
+Iff.intro
+(λ h, match d₁, d₂ with
+      | isTrue h₁,  isTrue h₂  := absurd (And.intro h₁ h₂) h
+      | _,           isFalse h₂ := Or.inr h₂
+      | isFalse h₁, _           := Or.inl h₁)
+(λ h ⟨hp, hq⟩, Or.elim h (λ h, h hp) (λ h, h hq))
+
+end Decidable
+
+section
+variables {p q : Prop}
+@[inline] def  decidableOfDecidableOfIff (hp : Decidable p) (h : p ↔ q) : Decidable q :=
+if hp : p then isTrue (Iff.mp h hp)
+else isFalse (Iff.mp (notIffNotOfIff h) hp)
+
+@[inline] def  decidableOfDecidableOfEq (hp : Decidable p) (h : p = q) : Decidable q :=
+decidableOfDecidableOfIff hp h.toIff
+end
+
+section
+variables {p q : Prop}
+
+@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∧ q) :=
+if hp : p then
+  if hq : q then isTrue ⟨hp, hq⟩
+  else isFalse (assume h : p ∧ q, hq (And.right h))
+else isFalse (assume h : p ∧ q, hp (And.left h))
+
+@[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∨ q) :=
+if hp : p then isTrue (Or.inl hp) else
+  if hq : q then isTrue (Or.inr hq) else
+    isFalse (λ h, Or.elim h hp hq)
+
+instance [Decidable p] : Decidable (¬p) :=
+if hp : p then isFalse (absurd hp) else isTrue hp
+
+@[macroInline] instance implies.Decidable [Decidable p] [Decidable q] : Decidable (p → q) :=
+if hp : p then
+  if hq : q then isTrue (assume h, hq)
+  else isFalse (assume h : p → q, absurd (h hp) hq)
+else isTrue (assume h, absurd h hp)
+
+instance [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
+if hp : p then
+  if hq : q then isTrue ⟨λ_, hq, λ_, hp⟩
+  else isFalse $ λh, hq (h.1 hp)
+else
+  if hq : q then isFalse $ λh, hp (h.2 hq)
+  else isTrue $ ⟨λh, absurd h hp, λh, absurd h hq⟩
+
+instance [Decidable p] [Decidable q] : Decidable (Xor p q) :=
+if hp : p then
+  if hq : q then isFalse (λ h, Or.elim h (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p)))
+  else isTrue $ Or.inl ⟨hp, hq⟩
+else
+  if hq : q then isTrue $ Or.inr ⟨hq, hp⟩
+  else isFalse (λ h, Or.elim h (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p)))
+
+end
+
+@[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) :=
+match decEq a b with
+| isTrue h := isFalse $ λ h', absurd h h'
+| isFalse h := isTrue h
+
+theorem Bool.falseNeTrue (h : false = true) : False :=
+Bool.noConfusion h
+
+instance : DecidableEq Bool :=
+{decEq := λ a b, match a, b with
+ | false, false := isTrue rfl
+ | false, true  := isFalse Bool.falseNeTrue
+ | true, false  := isFalse (Ne.symm Bool.falseNeTrue)
+ | true, true   := isTrue rfl}
+
+/- if-then-else expression theorems -/
+
+theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t :=
+match h with
+| (isTrue  hc)  := rfl
+| (isFalse hnc) := absurd hc hnc
+
+theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e :=
+match h with
+| (isTrue hc)   := absurd hc hnc
+| (isFalse hnc) := rfl
+
+-- Remark: dite and ite are "defally equal" when we ignore the proofs.
+theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (λ h, t) (λ h, e) = ite c t e :=
+match h with
+| (isTrue hc)   := rfl
+| (isFalse hnc) := rfl
+
+instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e)  :=
+match dC with
+| (isTrue hc)  := dT
+| (isFalse hc) := dE
+
+instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h)  :=
+match dC with
+| (isTrue hc)  := dT hc
+| (isFalse hc) := dE hc
+
+/-- Universe lifting operation -/
+structure {r s} ULift (α : Type s) : Type (max s r) :=
+up :: (down : α)
+
+namespace ULift
+/- Bijection between α and ULift.{v} α -/
+theorem upDown {α : Type u} : ∀ (b : ULift.{v} α), up (down b) = b
+| (up a) := rfl
+
+theorem downUp {α : Type u} (a : α) : down (up.{v} a) = a := rfl
+end ULift
+
+/-- Universe lifting operation from Sort to Type -/
+structure PLift (α : Sort u) : Type u :=
+up :: (down : α)
+
+namespace PLift
+/- Bijection between α and PLift α -/
+theorem upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b
+| (up a) := rfl
+
+theorem downUp {α : Sort u} (a : α) : down (up a) = a := rfl
+end PLift
+
+/- pointed types -/
+structure PointedType :=
+(type : Type u) (val : type)
+
+/- Inhabited -/
+
+class Inhabited (α : Sort u) :=
+(default : α)
+
+constant default (α : Sort u) [Inhabited α] : α :=
+Inhabited.default α
+
+@[inline, irreducible] def arbitrary (α : Sort u) [Inhabited α] : α :=
+default α
+
+instance Prop.Inhabited : Inhabited Prop :=
+⟨True⟩
+
+instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabited (α → β) :=
+Inhabited.casesOn h (λ b, ⟨λ a, b⟩)
+
+instance Pi.Inhabited (α : Sort u) {β : α → Sort v} [Π x, Inhabited (β x)] : Inhabited (Π x, β x) :=
+⟨λ a, default (β a)⟩
+
+instance : Inhabited Bool := ⟨false⟩
+
+instance : Inhabited True := ⟨trivial⟩
+
+instance : Inhabited Nat := ⟨0⟩
+
+instance : Inhabited NonScalar := ⟨⟨default _⟩⟩
+
+instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩
+
+class inductive Nonempty (α : Sort u) : Prop
+| intro (val : α) : Nonempty
+
+protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
+Nonempty.rec h₂ h₁
+
+instance nonemptyOfInhabited {α : Sort u} [Inhabited α] : Nonempty α :=
+⟨default α⟩
+
+theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : (∃ x, p x) → Nonempty α
+| ⟨w, h⟩ := ⟨w⟩
+
+/- Subsingleton -/
+
+class inductive Subsingleton (α : Sort u) : Prop
+| intro (h : ∀ a b : α, a = b) : Subsingleton
+
+protected def Subsingleton.elim {α : Sort u} [h : Subsingleton α] : ∀ (a b : α), a = b :=
+Subsingleton.casesOn h (λ p, p)
+
+protected def Subsingleton.helim {α β : Sort u} [h : Subsingleton α] (h : α = β) : ∀ (a : α) (b : β), a ≅ b :=
+Eq.recOn h (λ a b : α, heqOfEq (Subsingleton.elim a b))
+
+instance subsingletonProp (p : Prop) : Subsingleton p :=
+⟨λ a b, proofIrrel a b⟩
+
+instance (p : Prop) : Subsingleton (Decidable p) :=
+Subsingleton.intro (λ d₁,
+  match d₁ with
+  | (isTrue t₁) := (λ d₂,
+    match d₂ with
+    | (isTrue t₂) := Eq.recOn (proofIrrel t₁ t₂) rfl
+    | (isFalse f₂) := absurd t₁ f₂)
+  | (isFalse f₁) := (λ d₂,
+    match d₂ with
+    | (isTrue t₂) := absurd t₂ f₁
+    | (isFalse f₂) := Eq.recOn (proofIrrel f₁ f₂) rfl))
+
+protected theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u}
+                                 [h₃ : Π (h : p), Subsingleton (h₁ h)] [h₄ : Π (h : ¬p), Subsingleton (h₂ h)]
+                                 : Subsingleton (Decidable.casesOn h h₂ h₁) :=
+match h with
+| (isTrue h)  := h₃ h
+| (isFalse h) := h₄ h
+
+section relation
+variables {α : Sort u} {β : Sort v} (r : β → β → Prop)
+local infix `≺`:50 := r
+
+def Reflexive := ∀ x, x ≺ x
+
+def Symmetric := ∀ {x y}, x ≺ y → y ≺ x
+
+def Transitive := ∀ {x y z}, x ≺ y → y ≺ z → x ≺ z
+
+def Equivalence := Reflexive r ∧ Symmetric r ∧ Transitive r
+
+def Total := ∀ x y, x ≺ y ∨ y ≺ x
+
+def mkEquivalence (rfl : Reflexive r) (symm : Symmetric r) (trans : Transitive r) : Equivalence r :=
+⟨rfl, @symm, @trans⟩
+
+def Irreflexive := ∀ x, ¬ x ≺ x
+
+def AntiSymmetric := ∀ {x y}, x ≺ y → y ≺ x → x = y
+
+def emptyRelation := λ a₁ a₂ : α, False
+
+def Subrelation (q r : β → β → Prop) := ∀ {x y}, q x y → r x y
+
+def InvImage (f : α → β) : α → α → Prop :=
+λ a₁ a₂, f a₁ ≺ f a₂
+
+theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) :=
+λ (a₁ a₂ a₃ : α) (h₁ : InvImage r f a₁ a₂) (h₂ : InvImage r f a₂ a₃), h h₁ h₂
+
+theorem InvImage.Irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f) :=
+λ (a : α) (h₁ : InvImage r f a a), h (f a) h₁
+
+inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop
+| base  : ∀ a b, r a b → TC a b
+| trans : ∀ a b c, TC a b → TC b c → TC a c
+
+@[elabAsEliminator]
+theorem {u1 u2} TC.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
+                (m₁ : ∀ (a b : α), r a b → C a b)
+                (m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
+                {a b : α} (h : TC r a b) : C a b :=
+@TC.rec α r (λ a b _, C a b) m₁ m₂ a b h
+
+@[elabAsEliminator]
+theorem {u1 u2} TC.ndrecOn {α : Sort u} {r : α → α → Prop} {C : α → α → Prop}
+                {a b : α} (h : TC r a b)
+                (m₁ : ∀ (a b : α), r a b → C a b)
+                (m₂ : ∀ (a b c : α), TC r a b → TC r b c → C a b → C b c → C a c)
+                : C a b :=
+@TC.rec α r (λ a b _, C a b) m₁ m₂ a b h
+
+end relation
+
+section binary
+variables {α : Type u} {β : Type v}
+variable f : α → α → α
+local infix * := f
+
+def Commutative        := ∀ a b, a * b = b * a
+def Associative        := ∀ a b c, (a * b) * c = a * (b * c)
+def RightCommutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a₂ = h (h b a₂) a₁
+def LeftCommutative  (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
+
+local infix `◾`:50 := Eq.trans
+
+theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
+assume hcomm hassoc, assume a b c,
+  Eq.symm (hassoc a b c)
+◾ (hcomm a b ▸ rfl : (a*b)*c = (b*a)*c)
+◾ hassoc b a c
+
+theorem rightComm : Commutative f → Associative f → RightCommutative f :=
+assume hcomm hassoc, assume a b c,
+  hassoc a b c
+◾ (hcomm b c ▸ rfl : a*(b*c) = a*(c*b))
+◾ Eq.symm (hassoc a c b)
+
+end binary
+
+/- Subtype -/
+
+namespace Subtype
+def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x, p x
+| ⟨a, h⟩ := ⟨a, h⟩
+
+variables {α : Type u} {p : α → Prop}
+
+theorem tagIrrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
+rfl
+
+protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
+| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
+
+theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a :=
+Subtype.eq rfl
+
+instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} :=
+⟨⟨a, h⟩⟩
+
+instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
+{decEq := λ ⟨a, h₁⟩ ⟨b, h₂⟩,
+  if h : a = b then isTrue (Subtype.eq h)
+  else isFalse (λ h', Subtype.noConfusion h' (λ h', absurd h' h))}
+end Subtype
+
+/- Sum -/
+
+infixr ⊕ := Sum
+
+section
+variables {α : Type u} {β : Type v}
+
+instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (α ⊕ β) :=
+⟨Sum.inl (default α)⟩
+
+instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (α ⊕ β) :=
+⟨Sum.inr (default β)⟩
+
+instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (α ⊕ β) :=
+{decEq := λ a b,
+ match a, b with
+ | (Sum.inl a), (Sum.inl b) := if h : a = b then isTrue (h ▸ rfl)
+                               else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
+ | (Sum.inr a), (Sum.inr b) := if h : a = b then isTrue (h ▸ rfl)
+                               else isFalse (λ h', Sum.noConfusion h' (λ h', absurd h' h))
+ | (Sum.inr a), (Sum.inl b) := isFalse (λ h, Sum.noConfusion h)
+ | (Sum.inl a), (Sum.inr b) := isFalse (λ h, Sum.noConfusion h)}
+end
+
+/- Product -/
+
+section
+variables {α : Type u} {β : Type v}
+
+instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
+⟨(default α, default β)⟩
+
+instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
+{decEq := λ ⟨a, b⟩ ⟨a', b'⟩,
+  match (decEq a a') with
+  | (isTrue e₁) :=
+    (match (decEq b b') with
+     | (isTrue e₂)  := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
+     | (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
+  | (isFalse n₁) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}
+
+instance [HasLess α] [HasLess β] : HasLess (α × β) :=
+⟨λ s t, s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩
+
+instance prodHasDecidableLt
+         [HasLess α] [HasLess β] [DecidableEq α] [DecidableEq β]
+         [Π a b : α, Decidable (a < b)] [Π a b : β, Decidable (a < b)]
+         : Π s t : α × β, Decidable (s < t) :=
+λ t s, Or.Decidable
+
+theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
+rfl
+end
+
+def {u₁ u₂ v₁ v₂} Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
+  (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
+| (a, b) := (f a, g b)
+
+/- Dependent products -/
+
+notation `Σ` binders `, ` r:(scoped p, Sigma p) := r
+notation `Σ'` binders `, ` r:(scoped p, PSigma p) := r
+
+theorem exOfPsig {α : Type u} {p : α → Prop} : (Σ' x, p x) → ∃ x, p x
+| ⟨x, hx⟩ := ⟨x, hx⟩
+
+section
+variables {α : Type u} {β : α → Type v}
+
+protected theorem Sigma.Eq : ∀ {p₁ p₂ : Σ a : α, β a} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
+| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
+end
+
+section
+variables {α : Sort u} {β : α → Sort v}
+
+protected theorem PSigma.Eq : ∀ {p₁ p₂ : PSigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
+| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
+end
+
+/- Universe polymorphic unit -/
+
+theorem punitEq (a b : PUnit) : a = b :=
+PUnit.recOn a (PUnit.recOn b rfl)
+
+theorem punitEqPUnit (a : PUnit) : a = () :=
+punitEq a ()
+
+instance : Subsingleton PUnit :=
+Subsingleton.intro punitEq
+
+instance : Inhabited PUnit :=
+⟨⟨⟩⟩
+
+instance : DecidableEq PUnit :=
+{decEq := λ a b, isTrue (punitEq a b)}
+
+/- Setoid -/
+
+class Setoid (α : Sort u) :=
+(r : α → α → Prop) (iseqv : Equivalence r)
+
+instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α :=
+⟨Setoid.r⟩
+
+namespace Setoid
+variables {α : Sort u} [Setoid α]
+
+theorem refl (a : α) : a ≈ a :=
+match Setoid.iseqv α with
+| ⟨hRefl, hSymm, hTrans⟩ := hRefl a
+
+theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
+match Setoid.iseqv α with
+| ⟨hRefl, hSymm, hTrans⟩ := hSymm hab
+
+theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
+match Setoid.iseqv α with
+| ⟨hRefl, hSymm, hTrans⟩ := hTrans hab hbc
+end Setoid
+
+/- Propositional extensionality -/
+
+axiom propext {a b : Prop} : (a ↔ b) → a = b
+
+theorem eqTrueIntro {a : Prop} (h : a) : a = True :=
+propext (iffTrueIntro h)
+
+theorem eqFalseIntro {a : Prop} (h : ¬a) : a = False :=
+propext (iffFalseIntro h)
+
+/- Quotients -/
+
+-- Iff can now be used to do substitutions in a calculation
+theorem iffSubst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
+Eq.subst (propext h₁) h₂
+
+namespace Quot
+axiom sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b
+
+attribute [elabAsEliminator] lift ind
+
+protected theorem liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ a b, r a b → f a = f b) (a : α) : lift f c (Quot.mk r a) = f a :=
+rfl
+
+protected theorem indBeta {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (p : ∀ a, β (Quot.mk r a)) (a : α) : (ind p (Quot.mk r a) : β (Quot.mk r a)) = p a :=
+rfl
+
+@[reducible, elabAsEliminator, inline]
+protected def liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : ∀ a b, r a b → f a = f b) : β :=
+lift f c q
+
+@[elabAsEliminator]
+protected theorem inductionOn {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r) (h : ∀ a, β (Quot.mk r a)) : β q :=
+ind h q
+
+theorem existsRep {α : Sort u} {r : α → α → Prop} (q : Quot r) : ∃ a : α, (Quot.mk r a) = q :=
+Quot.inductionOn q (λ a, ⟨a, rfl⟩)
+
+section
+variable {α : Sort u}
+variable {r : α → α → Prop}
+variable {β : Quot r → Sort v}
+
+local notation `⟦`:max a `⟧` := Quot.mk r a
+
+@[reducible, macroInline]
+protected def indep (f : Π a, β ⟦a⟧) (a : α) : PSigma β :=
+⟨⟦a⟧, f a⟩
+
+protected theorem indepCoherent (f : Π a, β ⟦a⟧)
+                     (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
+                     : ∀ a b, r a b → Quot.indep f a = Quot.indep f b  :=
+λ a b e, PSigma.Eq (sound e) (h a b e)
+
+protected theorem liftIndepPr1
+  (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
+  (q : Quot r) : (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q  :=
+Quot.ind (λ (a : α), Eq.refl (Quot.indep f a).1) q
+
+@[reducible, elabAsEliminator, inline]
+protected def rec
+   (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
+   (q : Quot r) : β q :=
+Eq.ndrecOn (Quot.liftIndepPr1 f h q) ((lift (Quot.indep f) (Quot.indepCoherent f h) q).2)
+
+@[reducible, elabAsEliminator, inline]
+protected def recOn
+   (q : Quot r) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b) : β q :=
+Quot.rec f h q
+
+@[reducible, elabAsEliminator, inline]
+protected def recOnSubsingleton
+   [h : ∀ a, Subsingleton (β ⟦a⟧)] (q : Quot r) (f : Π a, β ⟦a⟧) : β q :=
+Quot.rec f (λ a b h, Subsingleton.elim _ (f b)) q
+
+@[reducible, elabAsEliminator, inline]
+protected def hrecOn
+   (q : Quot r) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q :=
+Quot.recOn q f $
+  λ a b p, eqOfHeq $
+    have p₁ : (Eq.rec (f a) (sound p) : β ⟦b⟧) ≅ f a, from eqRecHeq (sound p) (f a),
+    Heq.trans p₁ (c a b p)
+
+end
+end Quot
+
+def Quotient {α : Sort u} (s : Setoid α) :=
+@Quot α Setoid.r
+
+namespace Quotient
+
+@[inline]
+protected def mk {α : Sort u} [s : Setoid α] (a : α) : Quotient s :=
+Quot.mk Setoid.r a
+
+notation `⟦`:max a `⟧`:0 := Quotient.mk a
+
+def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → ⟦a⟧ = ⟦b⟧ :=
+Quot.sound
+
+@[reducible, elabAsEliminator]
+protected def lift {α : Sort u} {β : Sort v} [s : Setoid α] (f : α → β) : (∀ a b, a ≈ b → f a = f b) → Quotient s → β :=
+Quot.lift f
+
+@[elabAsEliminator]
+protected theorem ind {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} : (∀ a, β ⟦a⟧) → ∀ q, β q :=
+Quot.ind
+
+@[reducible, elabAsEliminator, inline]
+protected def liftOn {α : Sort u} {β : Sort v} [s : Setoid α] (q : Quotient s) (f : α → β) (c : ∀ a b, a ≈ b → f a = f b) : β :=
+Quot.liftOn q f c
+
+@[elabAsEliminator]
+protected theorem inductionOn {α : Sort u} [s : Setoid α] {β : Quotient s → Prop} (q : Quotient s) (h : ∀ a, β ⟦a⟧) : β q :=
+Quot.inductionOn q h
+
+theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : ∃ a : α, ⟦a⟧ = q :=
+Quot.existsRep q
+
+section
+variable {α : Sort u}
+variable [s : Setoid α]
+variable {β : Quotient s → Sort v}
+
+@[inline]
+protected def rec
+   (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b)
+   (q : Quotient s) : β q :=
+Quot.rec f h q
+
+@[reducible, elabAsEliminator, inline]
+protected def recOn
+   (q : Quotient s) (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β ⟦b⟧) = f b) : β q :=
+Quot.recOn q f h
+
+@[reducible, elabAsEliminator, inline]
+protected def recOnSubsingleton
+   [h : ∀ a, Subsingleton (β ⟦a⟧)] (q : Quotient s) (f : Π a, β ⟦a⟧) : β q :=
+@Quot.recOnSubsingleton _ _ _ h q f
+
+@[reducible, elabAsEliminator, inline]
+protected def hrecOn
+   (q : Quotient s) (f : Π a, β ⟦a⟧) (c : ∀ (a b : α) (p : a ≈ b), f a ≅ f b) : β q :=
+Quot.hrecOn q f c
+end
+
+section
+universes uA uB uC
+variables {α : Sort uA} {β : Sort uB} {φ : Sort uC}
+variables [s₁ : Setoid α] [s₂ : Setoid β]
+include s₁ s₂
+
+@[reducible, elabAsEliminator, inline]
+protected def lift₂
+   (f : α → β → φ)(c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
+   (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ :=
+Quotient.lift
+  (λ (a₁ : α), Quotient.lift (f a₁) (λ (a b : β), c a₁ a a₁ b (Setoid.refl a₁)) q₂)
+  (λ (a b : α) (h : a ≈ b),
+     @Quotient.ind β s₂
+       (λ (a1 : Quotient s₂),
+          (Quotient.lift (f a) (λ (a1 b : β), c a a1 a b (Setoid.refl a)) a1)
+          =
+          (Quotient.lift (f b) (λ (a b1 : β), c b a b b1 (Setoid.refl b)) a1))
+       (λ (a' : β), c a a' b a' h (Setoid.refl a'))
+       q₂)
+  q₁
+
+@[reducible, elabAsEliminator, inline]
+protected def liftOn₂
+  (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ a₁ a₂ b₁ b₂, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) : φ :=
+Quotient.lift₂ f c q₁ q₂
+
+@[elabAsEliminator]
+protected theorem ind₂ {φ : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ q₁ q₂ :=
+Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁
+
+@[elabAsEliminator]
+protected theorem inductionOn₂
+   {φ : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ :=
+Quotient.ind (λ a₁, Quotient.ind (λ a₂, h a₁ a₂) q₂) q₁
+
+@[elabAsEliminator]
+protected theorem inductionOn₃
+   [s₃ : Setoid φ]
+   {δ : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ a b c, δ ⟦a⟧ ⟦b⟧ ⟦c⟧)
+   : δ q₁ q₂ q₃ :=
+Quotient.ind (λ a₁, Quotient.ind (λ a₂, Quotient.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁
+end
+
+section exact
+variable   {α : Sort u}
+variable   [s : Setoid α]
+include s
+
+private def rel (q₁ q₂ : Quotient s) : Prop :=
+Quotient.liftOn₂ q₁ q₂
+  (λ a₁ a₂, a₁ ≈ a₂)
+  (λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂,
+    propext (Iff.intro
+      (λ a₁a₂, Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
+      (λ b₁b₂, Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
+
+local infix `~` := rel
+
+private theorem rel.refl : ∀ q : Quotient s, q ~ q :=
+λ q, Quot.inductionOn q (λ a, Setoid.refl a)
+
+private theorem eqImpRel {q₁ q₂ : Quotient s} : q₁ = q₂ → q₁ ~ q₂ :=
+assume h, Eq.ndrecOn h (rel.refl q₁)
+
+theorem exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
+assume h, eqImpRel h
+end exact
+
+section
+universes uA uB uC
+variables {α : Sort uA} {β : Sort uB}
+variables [s₁ : Setoid α] [s₂ : Setoid β]
+include s₁ s₂
+
+@[reducible, elabAsEliminator]
+protected def recOnSubsingleton₂
+   {φ : Quotient s₁ → Quotient s₂ → Sort uC} [h : ∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)]
+   (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : Π a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂:=
+@Quotient.recOnSubsingleton _ s₁ (λ q, φ q q₂) (λ a, Quotient.ind (λ b, h a b) q₂) q₁
+  (λ a, Quotient.recOnSubsingleton q₂ (λ b, f a b))
+
+end
+end Quotient
+
+section
+variable {α : Type u}
+variable (r : α → α → Prop)
+
+inductive EqvGen : α → α → Prop
+| rel {} : Π x y, r x y → EqvGen x y
+| refl {} : Π x, EqvGen x x
+| symm {} : Π x y, EqvGen x y → EqvGen y x
+| trans {} : Π x y z, EqvGen x y → EqvGen y z → EqvGen x z
+
+theorem EqvGen.isEquivalence : Equivalence (@EqvGen α r) :=
+mkEquivalence _ EqvGen.refl EqvGen.symm EqvGen.trans
+
+def EqvGen.Setoid : Setoid α :=
+Setoid.mk _ (EqvGen.isEquivalence r)
+
+theorem Quot.exact {a b : α} (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
+@Quotient.exact _ (EqvGen.Setoid r) a b (@congrArg _ _ _ _
+  (Quot.lift (@Quotient.mk _ (EqvGen.Setoid r)) (λx y h, Quot.sound (EqvGen.rel x y h))) H)
+
+theorem Quot.eqvGenSound {r : α → α → Prop} {a b : α} (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
+EqvGen.recOn H
+  (λ x y h, Quot.sound h)
+  (λ x, rfl)
+  (λ x y _ IH, Eq.symm IH)
+  (λ x y z _ _ IH₁ IH₂, Eq.trans IH₁ IH₂)
+end
+
+instance {α : Sort u} {s : Setoid α} [d : ∀ a b : α, Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
+{decEq := λ q₁ q₂ : Quotient s,
+  Quotient.recOnSubsingleton₂ q₁ q₂
+    (λ a₁ a₂,
+      match (d a₁ a₂) with
+      | (isTrue h₁)  := isTrue (Quotient.sound h₁)
+      | (isFalse h₂) := isFalse (λ h, absurd (Quotient.exact h) h₂))}
+
+/- Function extensionality -/
+
+namespace Function
+variables {α : Sort u} {β : α → Sort v}
+
+protected def Equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
+
+local infix `~` := Function.Equiv
+
+protected theorem Equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl
+
+protected theorem Equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ :=
+λ h x, Eq.symm (h x)
+
+protected theorem Equiv.trans {f₁ f₂ f₃ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
+λ h₁ h₂ x, Eq.trans (h₁ x) (h₂ x)
+
+protected theorem Equiv.isEquivalence (α : Sort u) (β : α → Sort v) : Equivalence (@Function.Equiv α β) :=
+mkEquivalence (@Function.Equiv α β) (@Equiv.refl α β) (@Equiv.symm α β) (@Equiv.trans α β)
+end Function
+
+section
+open Quotient
+variables {α : Sort u} {β : α → Sort v}
+
+@[instance]
+private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (Π x : α, β x) :=
+Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β)
+
+private def extfunApp (f : Quotient $ funSetoid α β) : Π x : α, β x :=
+assume x,
+Quot.liftOn f
+  (λ f : Π x : α, β x, f x)
+  (λ f₁ f₂ h, h x)
+
+theorem funext {f₁ f₂ : Π x : α, β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
+show extfunApp ⟦f₁⟧ = extfunApp ⟦f₂⟧, from
+congrArg extfunApp (sound h)
+end
+
+local infix `~` := Function.Equiv
+
+instance Pi.Subsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (Π a, β a) :=
+⟨λ f₁ f₂, funext (λ a, Subsingleton.elim (f₁ a) (f₂ a))⟩
+
+/- General operations on functions -/
+namespace Function
+universes u₁ u₂ u₃ u₄
+variables {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁}
+
+@[inline, reducible] def comp (f : β → φ) (g : α → β) : α → φ :=
+λ x, f (g x)
+
+infixr  ` ∘ `      := Function.comp
+
+@[inline, reducible] def onFun (f : β → β → φ) (g : α → β) : α → α → φ :=
+λ x y, f (g x) (g y)
+
+@[inline, reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ)
+  : α → β → ζ :=
+λ x y, op (f x y) (g x y)
+
+@[inline, reducible] def const (β : Sort u₂) (a : α) : β → α :=
+λ x, a
+
+@[inline, reducible] def swap {φ : α → β → Sort u₃} (f : Π x y, φ x y) : Π y x, φ x y :=
+λ y x, f x y
+
+infixl  ` on `:2         := onFun
+notation f ` -[` op `]- ` g  := combine f op g
+
+end Function
+
+/- Classical reasoning support -/
+
+namespace Classical
+
+axiom choice {α : Sort u} : Nonempty α → α
+
+noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop)
+  (h : ∃ x, p x) : {x // p x} :=
+choice $ let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩
+
+noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
+(indefiniteDescription p h).val
+
+theorem chooseSpec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
+(indefiniteDescription p h).property
+
+/- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
+theorem em (p : Prop) : p ∨ ¬p :=
+let U (x : Prop) : Prop := x = True ∨ p in
+let V (x : Prop) : Prop := x = False ∨ p in
+have exU : ∃ x, U x, from ⟨True, Or.inl rfl⟩,
+have exV : ∃ x, V x, from ⟨False, Or.inl rfl⟩,
+let u : Prop := choose exU in
+let v : Prop := choose exV in
+have uDef : U u, from chooseSpec exU,
+have vDef : V v, from chooseSpec exV,
+have notUvOrP : u ≠ v ∨ p, from
+  Or.elim uDef
+    (assume hut : u = True,
+      Or.elim vDef
+        (assume hvf : v = False,
+          have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse,
+          Or.inl hne)
+        Or.inr)
+    Or.inr,
+have pImpliesUv : p → u = v, from
+  assume hp : p,
+  have hpred : U = V, from
+    funext $ assume x : Prop,
+      have hl : (x = True ∨ p) → (x = False ∨ p), from
+        assume a, Or.inr hp,
+      have hr : (x = False ∨ p) → (x = True ∨ p), from
+        assume a, Or.inr hp,
+      show (x = True ∨ p) = (x = False ∨ p), from
+        propext (Iff.intro hl hr),
+  have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV, from
+    hpred ▸ λ exU exV, rfl,
+  show u = v, from h₀ _ _,
+Or.elim notUvOrP
+  (assume hne : u ≠ v, Or.inr (mt pImpliesUv hne))
+  Or.inl
+
+theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → ∃ x : α, True
+| ⟨x⟩ := ⟨x, trivial⟩
+
+noncomputable def inhabitedOfNonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
+⟨choice h⟩
+
+noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) :
+  Inhabited α :=
+inhabitedOfNonempty (Exists.elim h (λ w hw, ⟨w⟩))
+
+/- all propositions are Decidable -/
+noncomputable def propDecidable (a : Prop) : Decidable a :=
+choice $ Or.elim (em a)
+  (assume ha, ⟨isTrue ha⟩)
+  (assume hna, ⟨isFalse hna⟩)
+local attribute [instance] propDecidable
+
+noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
+⟨propDecidable a⟩
+local attribute [instance] decidableInhabited
+
+noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
+{decEq := λ x y, propDecidable (x = y)}
+
+noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
+match (propDecidable (Nonempty α)) with
+| (isTrue hp)  := PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp))
+| (isFalse hn) := PSum.inr (λ a, absurd (Nonempty.intro a) hn)
+
+noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
+  (h : Nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
+if hp : ∃ x : α, p x then
+  let xp := indefiniteDescription _ hp in
+  ⟨xp.val, λ h', xp.property⟩
+else ⟨choice h, λ h, absurd h hp⟩
+
+/- the Hilbert epsilon Function -/
+
+noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
+(strongIndefiniteDescription p h).val
+
+theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop)
+  : (∃ y, p y) → p (@epsilon α h p) :=
+(strongIndefiniteDescription p h).property
+
+theorem epsilonSpec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) :
+    p (@epsilon α (nonemptyOfExists hex) p) :=
+epsilonSpecAux (nonemptyOfExists hex) p hex
+
+theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y = x) = x :=
+@epsilonSpec α (λ y, y = x) ⟨x, rfl⟩
+
+/- the axiom of choice -/
+
+theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
+  ∃ (f : Π x, β x), ∀ x, r x (f x) :=
+⟨_, λ x, chooseSpec (h x)⟩
+
+theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
+  (∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, b x), ∀ x, p x (f x) :=
+⟨axiomOfChoice, λ ⟨f, hw⟩ x, ⟨f x, hw x⟩⟩
+
+theorem propComplete (a : Prop) : a = True ∨ a = False :=
+Or.elim (em a)
+  (λ t, Or.inl (eqTrueIntro t))
+  (λ f, Or.inr (eqFalseIntro f))
+
+-- this supercedes byCases in Decidable
+theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
+Decidable.byCases hpq hnpq
+
+-- this supercedes byContradiction in Decidable
+theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
+Decidable.byContradiction h
+
+end Classical