From 549912bbf4d21cfb115bfdf5f96b56f82f3cd17f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 8 Oct 2020 15:52:27 +0200
Subject: [PATCH] test: Reformat.lean: make output test

---
 tests/lean/Format.lean                |    2 +-
 tests/lean/{run => }/Reformat.lean    |    2 +-
 tests/lean/Reformat.lean.expected.out | 2230 +++++++++++++++++++++++++
 3 files changed, 2232 insertions(+), 2 deletions(-)
 rename tests/lean/{run => }/Reformat.lean (95%)
 create mode 100644 tests/lean/Reformat.lean.expected.out

diff --git a/tests/lean/Format.lean b/tests/lean/Format.lean
index 629fae9cef..553f8a6bb3 100644
--- a/tests/lean/Format.lean
+++ b/tests/lean/Format.lean
@@ -3,7 +3,7 @@ open Lean
 open Lean.Format
 
 def eval (w : Nat) (f : Format) : IO Unit := do
-IO.println $ be w 0 "" [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0 }] }]
+IO.println $ f.prettyAux w
 
 -- hard line breaks should re-evaluate flattening behavior within group
 #eval eval 5 $ group (text "a" ++ line ++ text "b\nlooooooooong" ++ line ++ text "c") ++ line ++ text "d"
diff --git a/tests/lean/run/Reformat.lean b/tests/lean/Reformat.lean
similarity index 95%
rename from tests/lean/run/Reformat.lean
rename to tests/lean/Reformat.lean
index bf867658fa..4c8fff78f2 100644
--- a/tests/lean/run/Reformat.lean
+++ b/tests/lean/Reformat.lean
@@ -23,4 +23,4 @@ if stx' != stx then
     if stx.getArg i != stx'.getArg i then
       throw $ IO.userError s!"reparsing failed:\n{stx.getArg i}\n{stx'.getArg i}"
 
-#eval main ["../../../src/Init/Core.lean"]
+#eval main ["../../src/Init/Core.lean"]
diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out
new file mode 100644
index 0000000000..d6904b10a8
--- /dev/null
+++ b/tests/lean/Reformat.lean.expected.out
@@ -0,0 +1,2230 @@
+prelude 
+
+notation `Prop` := Sort 0
+
+reserve infixr ` $ `:1
+
+notation f ` $ ` a := f a 
+
+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 infixr ` ▸ `:75
+
+reserve infixr ` × `:35
+
+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
+
+reserve prefix `!`:40
+
+reserve infixl ` && `:35
+
+reserve infixl ` || `:30
+
+reserve infixl ` ++ `:65
+
+reserve infixr ` :: `:67
+
+reserve infixr ` <|> `:2
+
+reserve infixl ` >>= `:55
+
+reserve infixr ` >=> `:55
+
+reserve infixl ` <*> `:60
+
+reserve infixl ` <* `:60
+
+reserve infixr ` *> `:60
+
+reserve infixr ` >> `:60
+
+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 : α → β → φ) : β → α → φ :=
+fun b a => f a b
+
+@[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
+
+@[macroInline, reducible]
+def idRhs (α : Sort u) (a : α) : α :=
+a
+
+/--Auxiliary Declaration used to implement the named patterns `x@p` -/
+@[reducible]
+def namedPattern {α : Sort u} (x 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
+
+@[matchPattern]
+abbrev Unit.unit : Unit :=
+PUnit.unit 
+
+structure Thunk(α : Type u) : Type u := 
+(fn : Unit → α)
+
+attribute [extern "lean_mk_thunk"] Thunk.mk
+
+@[noinline, extern "lean_thunk_pure"]
+protected def Thunk.pure {α : Type u} (a : α) : Thunk α :=
+⟨fun _ => a⟩
+
+@[noinline, extern "lean_thunk_get_own"]
+protected def Thunk.get {α : Type u} (x : @&Thunk α) : α :=
+x.fn ()
+
+@[noinline, extern "lean_thunk_map"]
+protected def Thunk.map {α : Type u} {β : Type v} (f : α → β) (x : Thunk α) : Thunk β :=
+⟨fun _ => f x.get⟩
+
+@[noinline, extern "lean_thunk_bind"]
+protected def Thunk.bind {α : Type u} {β : Type v} (x : Thunk α) (f : α → Thunk β) : Thunk β :=
+⟨fun _ => (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 Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
+@Eq.rec α a (fun α _ => C α) m b h
+
+@[elabAsEliminator, inline, reducible]
+def Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : Eq a b) (m : C a) : C b :=
+@Eq.rec α a (fun α _ => C α) m b h 
+
+init_quot 
+
+inductive HEq {α : Sort u} (a : α) : ∀  {β : Sort u}, β → Prop
+| refl{} : HEq a 
+
+structure Prod(α : Type u)(β : Type v) := 
+(fst : α)
+(snd : β)
+
+attribute [unbox] Prod
+
+/--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)
+
+infix `=` := Eq
+
+@[matchPattern]
+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
+
+@[matchPattern]
+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' :=
+  fun (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') => HEq.recOn h₁ (fun (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)
+
+attribute [unbox] Sigma 
+
+structure PSigma{α : Sort u}(β : α → Sort v) := mk :: 
+(fst : α)
+(snd : β fst)
+
+inductive Bool : Type
+| false : Bool
+| true : Bool 
+
+structure Subtype{α : Sort u}(p : α → Prop) := 
+(val : α)
+(property : p val)
+
+inductive Exists {α : Sort u} (p : α → Prop) : Prop
+| intro (w : α) (h : p w) : Exists 
+
+inductive ForInStep (α : Type u)
+| done : α → ForInStep
+| yield : α → ForInStep 
+
+inductive DoResultPRBC (α β σ : Type u)
+| «pure» : α → σ → DoResultPRBC
+| «return» : β → σ → DoResultPRBC
+| «break» : σ → DoResultPRBC
+| «continue» : σ → DoResultPRBC 
+
+inductive DoResultPR (α β σ : Type u)
+| «pure» : α → σ → DoResultPR
+| «return» : β → σ → DoResultPR 
+
+inductive DoResultBC (σ : Type u)
+| «break» : σ → DoResultBC
+| «continue» : σ → DoResultBC 
+
+inductive DoResultSBC (α σ : Type u)
+| «pureReturn» : α → σ → DoResultSBC
+| «break» : σ → DoResultSBC
+| «continue» : σ → DoResultSBC 
+
+class inductive Decidable (p : Prop)
+  | isFalse (h : ¬p) : Decidable
+  | isTrue (h : p) : Decidable 
+
+abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
+∀  (a : α), Decidable (r a)
+
+abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=
+∀  (a b : α), Decidable (r a b)
+
+abbrev DecidableEq (α : Sort u) :=
+∀  (a b : α), Decidable (a = b)
+
+def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
+s a b 
+
+inductive Option (α : Type u)
+| none : Option
+| some (val : α) : Option 
+
+attribute [unbox] 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 
+
+inductive Nat
+| zero : Nat
+| succ (n : Nat) : Nat 
+
+axiom sorryAx (α : Sort u) (synthetic := true) : α 
+
+class HasZero(α : Type u) := mk{} :: 
+(zero : α)
+
+class HasOne(α : Type u) := mk{} :: 
+(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 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 HasEquiv(α : Sort u) := 
+(Equiv : α → α → Prop)
+
+class HasEmptyc(α : Type u) := 
+(emptyc : α)
+
+class HasPow(α : Type u)(β : Type v) := 
+(pow : α → β → α)
+
+infix `+` := HasAdd.add 
+
+infix `*` := HasMul.mul 
+
+infix `-` := HasSub.sub 
+
+infix `/` := HasDiv.div 
+
+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 `≈` := HasEquiv.Equiv 
+
+infixr `^` := HasPow.pow 
+
+infixr `/\` := And 
+
+infixr `∧` := And 
+
+infixr `\/` := Or 
+
+infixr `∨` := Or 
+
+infix `<->` := Iff 
+
+infix `↔` := Iff 
+
+infixr `<|>` := HasOrelse.orelse 
+
+infixr `>>` := HasAndthen.andthen
+
+@[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
+
+@[inline]
+def bit0 {α : Type u} [s : HasAdd α] (a : α) : α :=
+a + a
+
+@[inline]
+def bit1 {α : Type u} [s₁ : HasOne α] [s₂ : HasAdd α] (a : α) : α :=
+(bit0 a) + 1
+
+attribute [matchPattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg
+
+@[extern "lean_nat_add"]
+protected def Nat.add : (@&Nat) → (@&Nat) → Nat
+| a, Nat.zero => a
+| a, Nat.succ b => Nat.succ (Nat.add a b)
+
+attribute [matchPattern] Nat.add Nat.add._main 
+
+instance  : HasZero Nat :=
+⟨Nat.zero⟩
+
+instance  : HasOne Nat :=
+⟨Nat.succ (Nat.zero)⟩
+
+instance  : HasAdd Nat :=
+⟨Nat.add⟩
+
+constant hugeFuel : Nat :=
+10000
+
+def std.priority.default : Nat :=
+1000
+
+def std.priority.max : Nat :=
+0xFFFFFFFF
+
+protected def Nat.prio :=
+std.priority.default + 100
+
+def std.prec.max : Nat :=
+1024
+
+def std.prec.arrow : Nat :=
+25
+
+def std.prec.maxPlus : Nat :=
+std.prec.max + 10
+
+structure Task(α : Type u) : Type u := pure :: 
+(get : α)
+
+attribute [extern "lean_task_pure"] Task.pure 
+
+attribute [extern "lean_task_get_own"] Task.get 
+
+namespace Task
+
+/--Task priority. Tasks with higher priority will always be scheduled before ones with lower priority. -/
+abbrev Priority :=
+Nat 
+
+def Priority.default : Priority :=
+0
+
+def Priority.max : Priority :=
+8
+
+/--Any priority higher than `Task.Priority.max` will result in the task being scheduled immediately on a dedicated thread.
+  This is particularly useful for long-running and/or I/O-bound tasks since Lean will by default allocate no more
+  non-dedicated workers than the number of cores to reduce context switches. -/
+def Priority.dedicated : Priority :=
+9
+
+@[noinline, extern "lean_task_spawn"]
+protected def spawn {α : Type u} (fn : Unit → α) (prio := Priority.default) : Task α :=
+⟨fn ()⟩
+
+@[noinline, extern "lean_task_map"]
+protected def map {α : Type u} {β : Type v} (f : α → β) (x : Task α) (prio := Priority.default) : Task β :=
+⟨f x.get⟩
+
+@[noinline, extern "lean_task_bind"]
+protected def bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β) (prio := Priority.default) : Task β :=
+⟨(f x.get).get⟩
+
+end Task 
+
+infixr `×` := Prod 
+
+structure NonScalar := 
+(val : Nat)
+
+inductive PNonScalar : Type u
+| mk (v : Nat) : PNonScalar 
+
+class HasOfNat(α : Type u) := 
+(ofNat : Nat → α)
+
+export HasOfNat(ofNat)
+
+instance  : HasOfNat Nat :=
+⟨id⟩
+
+class HasSizeof(α : Sort u) := 
+(sizeof : α → Nat)
+
+export HasSizeof(sizeof)
+
+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
+
+@[macroInline]
+def cond {a : Type u} : Bool → a → a → a
+| true, x, y => x
+| false, x, y => y
+
+@[inline]
+def condEq {β : Sort u} (b : Bool) (h₁ : b = true → β) (h₂ : b = false → β) : β :=
+@Bool.casesOn (λ x => b = x → β) b h₂ h₁ rfl
+
+@[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 c inline "#1 || #2"]
+def strictOr (b₁ b₂ : Bool) :=
+b₁ || b₂
+
+@[extern c inline "#1 && #2"]
+def strictAnd (b₁ b₂ : Bool) :=
+b₁ && b₂
+
+@[inline]
+def bne {α : Type u} [HasBeq α] (a b : α) : Bool :=
+!(a == b)
+
+infix `!=` := bne 
+
+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 :=
+fun hp => h₂ (h₁ hp)
+
+def trivial : True :=
+⟨⟩
+
+@[macroInline]
+def False.elim {C : Sort u} (h : False) : C :=
+False.rec (fun _ => 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 :=
+fun ha => h₂ (h₁ ha)
+
+theorem notFalse : ¬False :=
+id 
+
+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} : (α = β) → β → α :=
+fun 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 :=
+fun 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 :=
+fun h₁ => h (h₁.symm)
+
+theorem falseOfNe : a ≠ a → False :=
+Ne.irrefl 
+
+theorem neFalseOfSelf : p → p ≠ False :=
+fun (hp : p) (h : p = False) => h ▸ hp 
+
+theorem neTrueOfNot : ¬p → p ≠ True :=
+fun (hnp : ¬p) (h : p = True) => (h ▸ 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)
+
+theorem neFalseOfEqTrue : ∀  {b : Bool}, b = true → b ≠ false
+| true, _ => fun h => Bool.noConfusion h
+| false, h => Bool.noConfusion h 
+
+theorem neTrueOfEqFalse : ∀  {b : Bool}, b = false → b ≠ true
+| true, h => Bool.noConfusion h
+| false, _ => fun h => Bool.noConfusion h 
+
+section 
+
+variables{α β φ : Sort u}{a a' : α}{b b' : β}{c : φ}
+
+@[elabAsEliminator]
+theorem
+  HEq.ndrec.{u1,
+  u2} {α : Sort u2} {a : α} {C : ∀  {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) :
+  C b :=
+@HEq.rec α a (fun β b _ => C b) m β b h
+
+@[elabAsEliminator]
+theorem
+  HEq.ndrecOn.{u1,
+  u2} {α : Sort u2} {a : α} {C : ∀  {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) :
+  C b :=
+@HEq.rec α a (fun β 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 :=
+fun ⟨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 
+
+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 (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
+
+theorem Iff.refl (a : Prop) : a ↔ a :=
+Iff.intro (fun h => h) (fun 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 (fun ha => Iff.mp h₂ (Iff.mp h₁ ha)) (fun 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 :=
+fun h₁ h₂ => have a ↔ b from Eq.subst h₂ (Iff.refl a);
+  absurd this h₁ 
+
+theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
+Iff.intro (fun (hna : ¬a) (hb : b) => hna (Iff.right h₁ hb)) (fun (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 (fun hl => trivial) (fun hr => h)
+
+theorem iffFalseIntro (h : ¬a) : a ↔ False :=
+Iff.intro h (False.rec (fun _ => a))
+
+theorem notNotIntro (ha : a) : ¬¬a :=
+fun hna => hna ha 
+
+theorem notTrue : (¬True) ↔ False :=
+iffFalseIntro (notNotIntro trivial)
+
+theorem resolveLeft {a b : Prop} (h : a ∨ b) (na : ¬a) : b :=
+Or.elim h (fun ha => absurd ha na) id 
+
+theorem negResolveLeft {a b : Prop} (h : ¬a ∨ b) (ha : a) : b :=
+Or.elim h (fun na => absurd ha na) id 
+
+theorem resolveRight {a b : Prop} (h : a ∨ b) (nb : ¬b) : a :=
+Or.elim h id (fun hb => absurd hb nb)
+
+theorem negResolveRight {a b : Prop} (h : a ∨ ¬b) (hb : b) : a :=
+Or.elim h id (fun nb => absurd hb nb)
+
+theorem
+  Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : Exists (fun x => p x)) (h₂ : ∀  (a : α), p a → b) :
+  b :=
+Exists.rec h₂ h₁
+
+@[inlineIfReduce, nospecialize]
+def Decidable.decide (p : Prop) [h : Decidable p] : Bool :=
+Decidable.casesOn h (fun h₁ => false) (fun h₂ => true)
+
+export Decidable(isTrue isFalse decide)
+
+instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α :=
+⟨fun a b => decide (a = b)⟩
+
+theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true :=
+match h with 
+| isTrue h => rfl
+| isFalse h => False.elim (Iff.mp notTrue h)
+
+theorem decideFalseEqFalse (h : Decidable False) : @decide False h = false :=
+match h with 
+| isFalse h => rfl
+| isTrue h => False.elim h 
+
+theorem decideEqTrue : ∀  {p : Prop} [s : Decidable p], p → decide p = true
+| _, isTrue _, _ => rfl
+| _, isFalse h₁, h₂ => absurd h₂ h₁ 
+
+theorem decideEqFalse : ∀  {p : Prop} [s : Decidable p], ¬p → decide p = false
+| _, isTrue h₁, h₂ => absurd h₁ h₂
+| _, isFalse h, _ => rfl 
+
+theorem ofDecideEqTrue {p : Prop} [s : Decidable p] : decide p = true → p :=
+fun h => match s with 
+  | isTrue h₁ => h₁
+  | isFalse h₁ => absurd h (neTrueOfEqFalse (decideEqFalse h₁))
+
+theorem ofDecideEqFalse {p : Prop} [s : Decidable p] : decide p = false → ¬p :=
+fun h => match s with 
+  | isTrue h₁ => absurd h (neFalseOfEqTrue (decideEqTrue h₁))
+  | isFalse h₁ => h₁
+
+/--Similar to `decide`, but uses an explicit instance -/
+@[inline]
+def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
+@decide p d 
+
+theorem toBoolUsingEqTrue {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
+@decideEqTrue _ d h 
+
+theorem ofBoolUsingEqTrue {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p :=
+@ofDecideEqTrue _ d h 
+
+theorem ofBoolUsingEqFalse {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p :=
+@ofDecideEqFalse _ d h 
+
+instance  : Decidable True :=
+isTrue trivial 
+
+instance  : Decidable False :=
+isFalse notFalse
+
+@[macroInline]
+def dite {α : Sort u} (c : Prop) [h : Decidable c] : (c → α) → (¬c → α) → α :=
+fun t e => Decidable.casesOn h e t
+
+@[macroInline]
+def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
+Decidable.casesOn h (fun hnc => e) (fun 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 (fun h => False.rec _ (h h₃)) (fun 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 (fun h => h₄) (fun 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 (fun np => False.elim (h np))
+
+theorem ofNotNot [Decidable p] : ¬¬p → p :=
+fun hnn => byContradiction (fun 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 (fun 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₁) (fun (h) ⟨hp, hq⟩ => Or.elim h (fun h => h hp) (fun 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 (fun h => hq (And.right h)) else
+  isFalse (fun h => 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 (fun 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 (fun h => hq) else isFalse (fun h => absurd (h hp) hq) else
+  isTrue (fun h => absurd h hp)
+
+instance  [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
+if
+  hp :
+  p then
+  if hq : q then isTrue ⟨fun _ => hq, fun _ => hp⟩ else isFalse $ fun h => hq (h.1 hp) else
+  if hq : q then isFalse $ fun h => hp (h.2 hq) else isTrue $ ⟨fun h => absurd h hp, fun h => absurd h hq⟩
+
+instance  [Decidable p] [Decidable q] : Decidable (Xor p q) :=
+if
+  hp :
+  p then
+  if
+    hq :
+    q then
+    isFalse (fun h => Or.elim h (fun ⟨_, h⟩ => h hq : ¬(p ∧ ¬q)) (fun ⟨_, h⟩ => h hp : ¬(q ∧ ¬p))) else
+    isTrue $ Or.inl ⟨hp, hq⟩ else
+  if
+    hq :
+    q then
+    isTrue $ Or.inr ⟨hq, hp⟩ else
+    isFalse (fun h => Or.elim h (fun ⟨h, _⟩ => hp h : ¬(p ∧ ¬q)) (fun ⟨h, _⟩ => hq h : ¬(q ∧ ¬p)))
+
+end 
+
+@[inline]
+instance  {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) :=
+match decEq a b with 
+| isTrue h => isFalse $ fun h' => absurd h h'
+| isFalse h => isTrue h 
+
+theorem Bool.falseNeTrue (h : false = true) : False :=
+Bool.noConfusion h
+
+@[inline]
+instance  : DecidableEq Bool :=
+fun 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 
+
+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 
+
+theorem difPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} : (dite c t e) = t hc :=
+match h with 
+| (isTrue hc) => rfl
+| (isFalse hnc) => absurd hc hnc 
+
+theorem difNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} : (dite c t e) = e hnc :=
+match h with 
+| (isTrue hc) => absurd hc hnc
+| (isFalse hnc) => rfl 
+
+theorem
+  difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) :
+  dite c (fun h => t) (fun 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 ULift.{r, s}(α : Type s) : Type (max s r) := up :: 
+(down : α)
+
+namespace ULift 
+
+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 
+
+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 
+
+structure PointedType := 
+(type : Type u)
+(val : type)
+
+class Inhabited(α : Sort u) := mk{} :: 
+(default : α)
+
+constant arbitrary (α : Sort u) [Inhabited α] : α :=
+Inhabited.default α 
+
+instance Prop.Inhabited : Inhabited Prop :=
+⟨True⟩
+
+instance Fun.Inhabited (α : Sort u) {β : Sort v} [h : Inhabited β] : Inhabited (α → β) :=
+Inhabited.casesOn h (fun b => ⟨fun a => b⟩)
+
+instance Forall.Inhabited (α : Sort u) {β : α → Sort v} [∀  x, Inhabited (β x)] : Inhabited (∀  x, β x) :=
+⟨fun a => arbitrary (β a)⟩
+
+instance  : Inhabited Bool :=
+⟨false⟩
+
+instance  : Inhabited True :=
+⟨trivial⟩
+
+instance  : Inhabited Nat :=
+⟨0⟩
+
+instance  : Inhabited NonScalar :=
+⟨⟨arbitrary _⟩⟩
+
+instance  : Inhabited PNonScalar.{u} :=
+⟨⟨arbitrary _⟩⟩
+
+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 α :=
+⟨arbitrary α⟩
+
+theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
+| ⟨w, h⟩ => ⟨w⟩
+
+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 (fun p => p)
+
+protected def Subsingleton.helim {α β : Sort u} [h : Subsingleton α] (h : α = β) : ∀  (a : α) (b : β), a ≅ b :=
+Eq.recOn h (fun a b => heqOfEq (Subsingleton.elim a b))
+
+instance subsingletonProp (p : Prop) : Subsingleton p :=
+⟨fun a b => proofIrrel a b⟩
+
+instance  (p : Prop) : Subsingleton (Decidable p) :=
+Subsingleton.intro $ fun d₁ => match d₁ with 
+    | (isTrue t₁) => fun d₂ => match d₂ with 
+        | (isTrue t₂) => Eq.recOn (proofIrrel t₁ t₂) rfl
+        | (isFalse f₂) => absurd t₁ f₂
+    | (isFalse f₁) => fun 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)
+
+def Reflexive :=
+∀  x, r x x 
+
+def Symmetric :=
+∀  {x y}, r x y → r y x 
+
+def Transitive :=
+∀  {x y z}, r x y → r y z → r x z 
+
+def Equivalence :=
+Reflexive r ∧ Symmetric r ∧ Transitive r 
+
+def Total :=
+∀  x y, r x y ∨ r y x 
+
+def mkEquivalence (rfl : Reflexive r) (symm : Symmetric r) (trans : Transitive r) : Equivalence r :=
+⟨rfl, @symm, @trans⟩
+
+def Irreflexive :=
+∀  x, ¬r x x 
+
+def AntiSymmetric :=
+∀  {x y}, r x y → r y x → x = y 
+
+def emptyRelation (a₁ a₂ : α) : Prop :=
+False 
+
+def Subrelation (q r : β → β → Prop) :=
+∀  {x y}, q x y → r x y 
+
+def InvImage (f : α → β) : α → α → Prop :=
+fun a₁ a₂ => r (f a₁) (f a₂)
+
+theorem InvImage.Transitive (f : α → β) (h : Transitive r) : Transitive (InvImage r f) :=
+fun (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) :=
+fun (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
+  TC.ndrec.{u1,
+  u2}
+    {α : 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 (fun a b _ => C a b) m₁ m₂ a b h
+
+@[elabAsEliminator]
+theorem
+  TC.ndrecOn.{u1,
+  u2}
+    {α : 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 (fun a b _ => C a b) m₁ m₂ a b h 
+
+end relation 
+
+section Binary 
+
+variables{α : Type u}{β : Type v}
+
+variable(f : α → α → α)
+
+def Commutative :=
+∀  a b, f a b = f b a 
+
+def Associative :=
+∀  a b c, f (f a b) c = f a (f 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)
+
+theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
+fun
+  hcomm
+  hassoc
+  a
+  b
+  c =>
+  ((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c)
+
+theorem rightComm : Commutative f → Associative f → RightCommutative f :=
+fun
+  hcomm
+  hassoc
+  a
+  b
+  c =>
+  ((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b))
+
+end Binary 
+
+namespace Subtype 
+
+def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun 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 } :=
+fun
+  ⟨a, h₁⟩
+  ⟨b, h₂⟩ =>
+  if h : a = b then isTrue (Subtype.eq h) else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
+
+end Subtype 
+
+section 
+
+variables{α : Type u}{β : Type v}
+
+instance Sum.inhabitedLeft [h : Inhabited α] : Inhabited (Sum α β) :=
+⟨Sum.inl (arbitrary α)⟩
+
+instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (Sum α β) :=
+⟨Sum.inr (arbitrary β)⟩
+
+instance  {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) :=
+fun a b => match a, b with 
+  |
+  (Sum.inl a),
+      (Sum.inl b) =>
+      if h : a = b then isTrue (h ▸ rfl) else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h))
+  |
+  (Sum.inr a),
+      (Sum.inr b) =>
+      if h : a = b then isTrue (h ▸ rfl) else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h))
+  | (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h)
+  | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h)
+
+end 
+
+section 
+
+variables{α : Type u}{β : Type v}
+
+instance  [Inhabited α] [Inhabited β] : Inhabited (Prod α β) :=
+⟨(arbitrary α, arbitrary β)⟩
+
+instance  [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
+fun ⟨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 (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))
+  | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))
+
+instance  [HasBeq α] [HasBeq β] : HasBeq (α × β) :=
+⟨fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂⟩
+
+instance  [HasLess α] [HasLess β] : HasLess (α × β) :=
+⟨fun 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) :=
+fun 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
+  Prod.map.{u₁,
+  u₂,
+  v₁,
+  v₂} {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) :
+  α₁ × β₁ → α₂ × β₂
+| (a, b) => (f a, g b)
+
+theorem exOfPsig {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
+| ⟨x, hx⟩ => ⟨x, hx⟩
+
+section 
+
+variables{α : Type u}{β : α → Type v}
+
+protected
+  theorem
+  Sigma.eq :
+  ∀  {p₁ p₂ : Sigma (fun 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 
+
+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 :=
+fun a b => isTrue (punitEq a b)
+
+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 
+
+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)
+
+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) : Exists (fun a => (Quot.mk r a) = q) :=
+Quot.inductionOn q (fun a => ⟨a, rfl⟩)
+
+section 
+
+variable{α : Sort u}
+
+variable{r : α → α → Prop}
+
+variable{β : Quot r → Sort v}
+
+@[reducible, macroInline]
+protected def indep (f : ∀  a, β (Quot.mk r a)) (a : α) : PSigma β :=
+⟨Quot.mk r a, f a⟩
+
+protected
+  theorem
+  indepCoherent
+    (f : ∀  a, β (Quot.mk r a))
+    (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) :
+  ∀  a b, r a b → Quot.indep f a = Quot.indep f b :=
+fun a b e => PSigma.eq (sound e) (h a b e)
+
+protected
+  theorem
+  liftIndepPr1
+    (f : ∀  a, β (Quot.mk r a))
+    (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b)
+    (q : Quot r) :
+  (lift (Quot.indep f) (Quot.indepCoherent f h) q).1 = q :=
+Quot.ind (fun (a : α) => Eq.refl (Quot.indep f a).1) q
+
+@[reducible, elabAsEliminator, inline]
+protected
+  def
+  rec
+    (f : ∀  a, β (Quot.mk r a))
+    (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r 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, β (Quot.mk r a))
+    (h : ∀  (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β (Quot.mk r b)) = f b) :
+  β q :=
+Quot.rec f h q
+
+@[reducible, elabAsEliminator, inline]
+protected
+  def
+  recOnSubsingleton [h : ∀  a, Subsingleton (β (Quot.mk r a))] (q : Quot r) (f : ∀  a, β (Quot.mk r a)) :
+  β q :=
+Quot.rec f (fun a b h => Subsingleton.elim _ (f b)) q
+
+@[reducible, elabAsEliminator, inline]
+protected def hrecOn (q : Quot r) (f : ∀  a, β (Quot.mk r a)) (c : ∀  (a b : α) (p : r a b), f a ≅ f b) : β q :=
+Quot.recOn q f $
+  fun a b p => eqOfHEq $ have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := 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 
+
+def sound {α : Sort u} [s : Setoid α] {a b : α} : a ≈ b → Quotient.mk a = Quotient.mk 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, β (Quotient.mk 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, β (Quotient.mk a)) :
+  β q :=
+Quot.inductionOn q h 
+
+theorem existsRep {α : Sort u} [s : Setoid α] (q : Quotient s) : Exists (fun (a : α) => Quotient.mk a = q) :=
+Quot.existsRep q 
+
+section 
+
+variable{α : Sort u}
+
+variable[s : Setoid α]
+
+variable{β : Quotient s → Sort v}
+
+@[inline]
+protected
+  def
+  rec
+    (f : ∀  a, β (Quotient.mk a))
+    (h : ∀  (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β (Quotient.mk b)) = f b)
+    (q : Quotient s) :
+  β q :=
+Quot.rec f h q
+
+@[reducible, elabAsEliminator, inline]
+protected
+  def
+  recOn
+    (q : Quotient s)
+    (f : ∀  a, β (Quotient.mk a))
+    (h : ∀  (a b : α) (p : a ≈ b), (Eq.rec (f a) (Quotient.sound p) : β (Quotient.mk b)) = f b) :
+  β q :=
+Quot.recOn q f h
+
+@[reducible, elabAsEliminator, inline]
+protected
+  def
+  recOnSubsingleton [h : ∀  a, Subsingleton (β (Quotient.mk a))] (q : Quotient s) (f : ∀  a, β (Quotient.mk a)) :
+  β q :=
+@Quot.recOnSubsingleton _ _ _ h q f
+
+@[reducible, elabAsEliminator, inline]
+protected def hrecOn (q : Quotient s) (f : ∀  a, β (Quotient.mk 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 β]
+
+@[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
+  (fun (a₁ : α) => Quotient.lift (f a₁) (fun (a b : β) => c a₁ a a₁ b (Setoid.refl a₁)) q₂)
+  (fun
+      (a b : α)
+      (h : a ≈ b) =>
+      @Quotient.ind
+        β
+        s₂
+        (fun
+            (a1 : Quotient s₂) =>
+            (Quotient.lift (f a) (fun (a1 b : β) => c a a1 a b (Setoid.refl a)) a1) =
+              (Quotient.lift (f b) (fun (a b1 : β) => c b a b b1 (Setoid.refl b)) a1))
+        (fun (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, φ (Quotient.mk a) (Quotient.mk b))
+    (q₁ : Quotient s₁)
+    (q₂ : Quotient s₂) :
+  φ q₁ q₂ :=
+Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => h a₁ a₂) q₂) q₁
+
+@[elabAsEliminator]
+protected
+  theorem
+  inductionOn₂
+    {φ : Quotient s₁ → Quotient s₂ → Prop}
+    (q₁ : Quotient s₁)
+    (q₂ : Quotient s₂)
+    (h : ∀  a b, φ (Quotient.mk a) (Quotient.mk b)) :
+  φ q₁ q₂ :=
+Quotient.ind (fun a₁ => Quotient.ind (fun 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, δ (Quotient.mk a) (Quotient.mk b) (Quotient.mk c)) :
+  δ q₁ q₂ q₃ :=
+Quotient.ind (fun a₁ => Quotient.ind (fun a₂ => Quotient.ind (fun a₃ => h a₁ a₂ a₃) q₃) q₂) q₁ 
+
+end 
+
+section Exact 
+
+variable{α : Sort u}
+
+private def rel [s : Setoid α] (q₁ q₂ : Quotient s) : Prop :=
+Quotient.liftOn₂
+  q₁
+  q₂
+  (fun a₁ a₂ => a₁ ≈ a₂)
+  (fun
+      a₁
+      a₂
+      b₁
+      b₂
+      a₁b₁
+      a₂b₂ =>
+      propext
+        (Iff.intro
+            (fun a₁a₂ => Setoid.trans (Setoid.symm a₁b₁) (Setoid.trans a₁a₂ a₂b₂))
+            (fun b₁b₂ => Setoid.trans a₁b₁ (Setoid.trans b₁b₂ (Setoid.symm a₂b₂)))))
+
+private theorem rel.refl [s : Setoid α] : ∀  (q : Quotient s), rel q q :=
+fun q => Quot.inductionOn q (fun a => Setoid.refl a)
+
+private theorem eqImpRel [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
+fun h => Eq.ndrecOn h (rel.refl q₁)
+
+theorem exact [s : Setoid α] {a b : α} : Quotient.mk a = Quotient.mk b → a ≈ b :=
+fun h => eqImpRel h 
+
+end Exact 
+
+section 
+
+universes uA uB uC 
+
+variables{α : Sort uA}{β : Sort uB}
+
+variables[s₁ : Setoid α][s₂ : Setoid β]
+
+@[reducible, elabAsEliminator]
+protected
+  def
+  recOnSubsingleton₂
+    {φ : Quotient s₁ → Quotient s₂ → Sort uC}
+    [h : ∀  a b, Subsingleton (φ (Quotient.mk a) (Quotient.mk b))]
+    (q₁ : Quotient s₁)
+    (q₂ : Quotient s₂)
+    (f : ∀  a b, φ (Quotient.mk a) (Quotient.mk b)) :
+  φ q₁ q₂ :=
+@Quotient.recOnSubsingleton
+  _
+  s₁
+  (fun q => φ q q₂)
+  (fun a => Quotient.ind (fun b => h a b) q₂)
+  q₁
+  (fun a => Quotient.recOnSubsingleton q₂ (fun 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)) (fun 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
+  (fun x y h => Quot.sound h)
+  (fun x => rfl)
+  (fun x y _ IH => Eq.symm IH)
+  (fun x y z _ _ IH₁ IH₂ => Eq.trans IH₁ IH₂)
+
+end 
+
+instance  {α : Sort u} {s : Setoid α} [d : ∀  (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
+fun (q₁ q₂ : Quotient s) => Quotient.recOnSubsingleton₂ q₁ q₂ (fun a₁ a₂ => match (d a₁ a₂) with 
+        | (isTrue h₁) => isTrue (Quotient.sound h₁)
+        | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂))
+
+namespace Function 
+
+variables{α : Sort u}{β : α → Sort v}
+
+def Equiv (f₁ f₂ : ∀  (x : α), β x) : Prop :=
+∀  x, f₁ x = f₂ x 
+
+protected theorem Equiv.refl (f : ∀  (x : α), β x) : Equiv f f :=
+fun x => rfl 
+
+protected theorem Equiv.symm {f₁ f₂ : ∀  (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₁ :=
+fun h x => Eq.symm (h x)
+
+protected theorem Equiv.trans {f₁ f₂ f₃ : ∀  (x : α), β x} : Equiv f₁ f₂ → Equiv f₂ f₃ → Equiv f₁ f₃ :=
+fun 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 :=
+fun x => Quot.liftOn f (fun (f : ∀  (x : α), β x) => f x) (fun f₁ f₂ h => h x)
+
+theorem funext {f₁ f₂ : ∀  (x : α), β x} (h : ∀  x, f₁ x = f₂ x) : f₁ = f₂ :=
+show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂) from congrArg extfunApp (sound h)
+
+end 
+
+instance Forall.Subsingleton {α : Sort u} {β : α → Sort v} [∀  a, Subsingleton (β a)] : Subsingleton (∀  a, β a) :=
+⟨fun f₁ f₂ => funext (fun a => Subsingleton.elim (f₁ a) (f₂ a))⟩
+
+namespace Function 
+
+universes u₁ u₂ u₃ u₄ 
+
+variables{α : Sort u₁}{β : Sort u₂}{φ : Sort u₃}{δ : Sort u₄}{ζ : Sort u₁}
+
+@[inline, reducible]
+def comp (f : β → φ) (g : α → β) : α → φ :=
+fun x => f (g x)
+
+infixr ` ∘ ` := Function.comp
+
+@[inline, reducible]
+def onFun (f : β → β → φ) (g : α → β) : α → α → φ :=
+fun x y => f (g x) (g y)
+
+@[inline, reducible]
+def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ) : α → β → ζ :=
+fun x y => op (f x y) (g x y)
+
+@[inline, reducible]
+def const (β : Sort u₂) (a : α) : β → α :=
+fun x => a
+
+@[inline, reducible]
+def swap {φ : α → β → Sort u₃} (f : ∀  x y, φ x y) : ∀  y x, φ x y :=
+fun y x => f x y 
+
+end Function 
+
+def Squash (α : Type u) :=
+Quot (fun (a b : α) => True)
+
+def Squash.mk {α : Type u} (x : α) : Squash α :=
+Quot.mk _ x 
+
+theorem Squash.ind {α : Type u} {β : Squash α → Prop} (h : ∀  (a : α), β (Squash.mk a)) : ∀  (q : Squash α), β q :=
+Quot.ind h
+
+@[inline]
+def Squash.lift {α β} [Subsingleton β] (s : Squash α) (f : α → β) : β :=
+Quot.lift f (fun a b _ => Subsingleton.elim _ _) s 
+
+instance Squash.Subsingleton {α} : Subsingleton (Squash α) :=
+⟨Squash.ind (fun (a : α) => Squash.ind (fun (b : α) => Quot.sound trivial))⟩
+
+namespace Lean
+
+/--When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
+  The kernel will not use the interpreter if `c` is not a constant.
+  This feature is useful for performing proofs by reflection.
+
+  Remark: the Lean frontend allows terms of the from `Lean.reduceBool t` where `t` is a term not containing
+  free variables. The frontend automatically declares a fresh auxiliary constant `c` and replaces the term with
+  `Lean.reduceBool c`. The main motivation is that the code for `t` will be pre-compiled.
+
+  Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
+  This is extra 30k lines of code. More importantly, you will probably not be able to check your developement using
+  external type checkers (e.g., Trepplein) that do not implement this feature.
+  Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
+  So, you are mainly losing the capability of type checking your developement using external checkers.
+
+  Recall that the compiler trusts the correctness of all `[implementedBy ...]` and `[extern ...]` annotations.
+  If an extern function is executed, then the trusted code base will also include the implementation of the associated
+  foreign function.
+-/
+constant reduceBool (b : Bool) : Bool :=
+b
+
+/--Similar to `Lean.reduceBool` for closed `Nat` terms.
+
+  Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
+  The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
+  We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
+constant reduceNat (n : Nat) : Nat :=
+n 
+
+axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b 
+
+axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b 
+
+end Lean 
+
+namespace Classical 
+
+axiom choice {α : Sort u} : Nonempty α → α 
+
+noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : Exists (fun x => p x)) : { x // p x } :=
+choice $ let ⟨x, px⟩ := h;
+  ⟨⟨x, px⟩⟩
+
+noncomputable def choose {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : α :=
+(indefiniteDescription p h).val 
+
+theorem chooseSpec {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : p (choose h) :=
+(indefiniteDescription p h).property 
+
+theorem em (p : Prop) : p ∨ ¬p :=
+let U (x : Prop) : Prop := x = True ∨ p;
+let V (x : Prop) : Prop := x = False ∨ p;
+have exU : Exists (fun x => U x) from ⟨True, Or.inl rfl⟩;
+have exV : Exists (fun x => V x) from ⟨False, Or.inl rfl⟩;
+let u : Prop := choose exU;
+let v : Prop := choose exV;
+have uDef : U u from chooseSpec exU;
+have vDef : V v from chooseSpec exV;
+have
+  notUvOrP :
+  u ≠ v ∨ p from
+  Or.elim uDef (fun hut => Or.elim vDef (fun hvf => have hne : u ≠ v from hvf.symm ▸ hut.symm ▸ trueNeFalse;
+              Or.inl hne) Or.inr) Or.inr;
+have
+  pImpliesUv :
+  p → u = v from
+  fun
+    hp =>
+    have hpred : U = V from funext $ fun x => have hl : (x = True ∨ p) → (x = False ∨ p) from fun a => Or.inr hp;
+          have hr : (x = False ∨ p) → (x = True ∨ p) from fun 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 ▸ fun exU exV => rfl;
+    show u = v from h₀ _ _;
+Or.elim notUvOrP (fun (hne : u ≠ v) => Or.inr (mt pImpliesUv hne)) Or.inl 
+
+theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → Exists (fun (x : α) => True)
+| ⟨x⟩ => ⟨x, trivial⟩
+
+noncomputable def inhabitedOfNonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
+⟨choice h⟩
+
+noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : Exists (fun x => p x)) : Inhabited α :=
+inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩))
+
+noncomputable def propDecidable (a : Prop) : Decidable a :=
+choice $ Or.elim (em a) (fun ha => ⟨isTrue ha⟩) (fun hna => ⟨isFalse hna⟩)
+
+noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
+⟨propDecidable a⟩
+
+noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
+fun x y => propDecidable (x = y)
+
+noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
+match (propDecidable (Nonempty α)) with 
+| (isTrue hp) => PSum.inl (@arbitrary _ (inhabitedOfNonempty hp))
+| (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn)
+
+noncomputable
+  def
+  strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) :
+  { x : α // Exists (fun (y : α) => p y) → p x } :=
+@dite
+  _
+  (Exists (fun (x : α) => p x))
+  (propDecidable _)
+  (fun
+      (hp : Exists (fun (x : α) => p x)) =>
+      show { x : α // Exists (fun (y : α) => p y) → p x } from let xp := indefiniteDescription _ hp;
+        ⟨xp.val, fun h' => xp.property⟩)
+  (fun hp => ⟨choice h, fun h => absurd h hp⟩)
+
+noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
+(strongIndefiniteDescription p h).val 
+
+theorem epsilonSpecAux {α : Sort u} (h : Nonempty α) (p : α → Prop) : Exists (fun y => p y) → p (@epsilon α h p) :=
+(strongIndefiniteDescription p h).property 
+
+theorem
+  epsilonSpec {α : Sort u} {p : α → Prop} (hex : Exists (fun y => p y)) :
+  p (@epsilon α (nonemptyOfExists hex) p) :=
+epsilonSpecAux (nonemptyOfExists hex) p hex 
+
+theorem epsilonSingleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
+@epsilonSpec α (fun y => y = x) ⟨x, rfl⟩
+
+theorem
+  axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀  x, β x → Prop} (h : ∀  x, Exists (fun y => r x y)) :
+  Exists (fun (f : ∀  x, β x) => ∀  x, r x (f x)) :=
+⟨_, fun x => chooseSpec (h x)⟩
+
+theorem
+  skolem {α : Sort u} {b : α → Sort v} {p : ∀  x, b x → Prop} :
+  (∀  x, Exists (fun y => p x y)) ↔ Exists (fun (f : ∀  x, b x) => ∀  x, p x (f x)) :=
+⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩
+
+theorem propComplete (a : Prop) : a = True ∨ a = False :=
+Or.elim (em a) (fun t => Or.inl (eqTrueIntro t)) (fun f => Or.inr (eqFalseIntro f))
+
+theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
+@Decidable.byCases _ _ (propDecidable _) hpq hnpq 
+
+theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
+@Decidable.byContradiction _ (propDecidable _) h 
+
+end Classical