diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
new file mode 100644
index 0000000000..1c19059237
--- /dev/null
+++ b/library/init/lean/elaborator.lean
@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sebastian Ullrich
+
+Elaborator for the Lean language
+-/
+prelude
+import init.lean.parser.module
+
+namespace lean
+namespace elaborator
+open parser
+open parser.term
+open parser.command
+open parser.command.notation_spec
+
+structure elaborator_config :=
+(filename : string)
+
+structure elaborator_state :=
+(reserved_notations : list reserve_notation.view := [])
+(parser_cfg : module_parser_config)
+
+@[derive monad monad_reader monad_state monad_except]
+def elaborator_m := reader_t elaborator_config $ state_t elaborator_state $ except_t message id
+abbreviation elaborator := syntax → elaborator_m unit
+
+def error {α : Type} (context : syntax) (text : string) : elaborator_m α :=
+do cfg ← read,
+   -- TODO(Sebastian): convert position
+   throw {filename := cfg.filename, pos := /-context.get_pos.get_or_else-/ ⟨1,0⟩, text := text}
+
+local attribute [instance] name.has_lt_quick
+
+def max_prec := 1024
+
+-- TODO(Sebastian): should these actually be macros?
+def preprocess_notation_spec (spec : notation_spec.view) : notation_spec.view :=
+-- default leading tokens to `max`
+match spec with
+| {prefix_arg := none, rules := r@{symbol := notation_symbol.view.quoted sym@{prec := none, ..}, ..}::rs} :=
+  {spec with rules := {r with symbol := notation_symbol.view.quoted {sym with prec := some {prec := number.view.of_nat max_prec}}}::rs}
+| _ := spec
+
+def reserve_notation.elaborate : elaborator :=
+λ stx, do
+  let v := view reserve_notation stx,
+  let v := {v with spec := preprocess_notation_spec v.spec},
+  -- TODO: sanity checks?
+  st ← get,
+  cfg ← match command_parser_config.register_notation_tokens v.spec st.parser_cfg with
+  | except.ok cfg  := pure cfg
+  | except.error e := error stx e,
+  put {st with reserved_notations := v::st.reserved_notations,
+    parser_cfg := {..cfg, ..st.parser_cfg}}
+
+def match_precedence : option precedence.view → option precedence.view → option precedence.view
+| none      (some rp) := pure rp
+| (some sp) (some rp) := guard (sp.prec.to_nat = rp.prec.to_nat) *> pure rp
+| _         _         := failure
+
+/-- Check if a notation is compatible with a reserved notation, and if so, copy missing
+    precedences in the notation from the reserved notation. -/
+def match_spec (spec reserved : notation_spec.view) : option notation_spec.view :=
+do guard $ spec.prefix_arg.is_some = reserved.prefix_arg.is_some,
+   rules ← (spec.rules.zip reserved.rules).mmap $ λ ⟨sr, rr⟩, do {
+     -- TODO(Sebastian): unquoted symbols?
+     notation_symbol.view.quoted sq@{symbol := syntax.atom sa, ..} ← pure sr.symbol
+       | failure,
+     notation_symbol.view.quoted rq@{symbol := syntax.atom ra, ..} ← pure rr.symbol
+       | failure,
+     guard $ sa.val = ra.val,
+     sp ← match_precedence sq.prec rq.prec,
+     st ← match sr.transition, rr.transition with
+     | some (transition.view.binder sb), some (transition.view.binder rb) :=
+       match_precedence sb.prec rb.prec <&> λ p, some $ transition.view.binder {sb with prec := p}
+     | some (transition.view.binders sb), some (transition.view.binders rb) :=
+       match_precedence sb.prec rb.prec <&> λ p, some $ transition.view.binders {sb with prec := p}
+     | some (transition.view.arg sarg), some (transition.view.arg rarg) := do
+       sact ← match action.view.action <$> sarg.action, action.view.action <$> rarg.action with
+       | some (action_kind.view.prec sp), some (action_kind.view.prec rp) :=
+         guard (sp.to_nat = rp.to_nat) *> pure sarg.action
+       | none,                            some (action_kind.view.prec rp) :=
+         pure rarg.action
+       | _, _ := failure,
+       pure $ some $ transition.view.arg {sarg with action := sact}
+     | none,    none    := pure none
+     | _,       _       := failure,
+     pure $ {rule.view .
+       symbol := notation_symbol.view.quoted {sq with prec := sp},
+       transition := st}
+   },
+   pure $ {spec with rules := rules}
+
+def notation.elaborate : elaborator :=
+λ stx, do
+  let nota := view «notation» stx,
+  let nota := {nota with spec := preprocess_notation_spec nota.spec},
+  st ← get,
+
+  -- check reserved notations
+  matched ← pure $ st.reserved_notations.filter_map $
+    λ rnota, match_spec nota.spec rnota.spec,
+  nota ← match matched with
+  | [matched] := pure {nota with spec := matched}
+  | []        := pure nota
+  | _         := error stx "invalid notation, matches multiple reserved notations",
+
+  cfg ← match command_parser_config.register_notation_tokens nota.spec st.parser_cfg >>=
+              command_parser_config.register_notation_parser nota.spec with
+  | except.ok cfg  := pure cfg
+  | except.error e := error stx e,
+  put {st with parser_cfg := {..cfg, ..st.parser_cfg}}
+
+-- TODO(Sebastian): replace with attribute
+def elaborators : rbmap name elaborator (<) := rbmap.from_list [
+  (notation.name, notation.elaborate),
+  (reserve_notation.name, reserve_notation.elaborate)
+] _
+
+def elaborate (stx : syntax) : elaborator_m unit :=
+do syntax.node {kind := some k, ..} ← pure stx | pure (),
+   some t ← pure $ elaborators.find k.name | pure (),
+   t stx
+
+end elaborator
+end lean
diff --git a/library/init/lean/parser/notation.lean b/library/init/lean/parser/notation.lean
index 6fe180894d..9ff8457684 100644
--- a/library/init/lean/parser/notation.lean
+++ b/library/init/lean/parser/notation.lean
@@ -113,5 +113,36 @@ node! «reserve_mixfix» [
   symbol: notation_spec.notation_symbol.parser]
 
 end «command»
+open «command»
+open command.notation_spec
+
+def command_parser_config.register_notation_tokens (spec : notation_spec.view) (cfg : command_parser_config) :
+  except string command_parser_config :=
+do spec.rules.mfoldl (λ (cfg : command_parser_config) r, match r.symbol with
+   | notation_symbol.view.quoted {symbol := syntax.atom a, prec := some prec, ..} :=
+     pure {cfg with tokens := cfg.tokens.insert a.val {«prefix» := a.val}}
+   | _ := throw "register_notation: unreachable") cfg
+
+def command_parser_config.register_notation_parser (spec : notation_spec.view) (cfg : command_parser_config) :
+  except string command_parser_config :=
+do -- build and register parser
+   let k : syntax_node_kind := {name := "notation<TODO>"},
+   ps ← spec.rules.mmap (λ r : rule.view, do
+     psym ← match r.symbol with
+     | notation_symbol.view.quoted {symbol := syntax.atom a ..} :=
+       pure (symbol a.val : term_parser)
+     | _ := throw "register_notation: unreachable",
+     ptrans ← match r.transition with
+     | some (transition.view.arg arg) := pure $ some term.parser
+     | none := pure $ none
+     | _ := throw "register_notation: unimplemented",
+     pure $ psym::ptrans.to_monad
+   ),
+   let ps := ps.bind id,
+   cfg ← match spec.prefix_arg with
+   | none   := pure {cfg with leading_term_parsers := node k ps::cfg.leading_term_parsers}
+   | some _ := pure {cfg with trailing_term_parsers := node k (read::ps.map coe)::cfg.trailing_term_parsers},
+   pure cfg
+
 end parser
 end lean
diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean
index 6a1ba862b8..4dd897c60c 100644
--- a/tests/lean/parser1.lean
+++ b/tests/lean/parser1.lean
@@ -1,7 +1,8 @@
-import init.lean.parser.module init.lean.expander init.io
+import init.lean.parser.module init.lean.expander init.lean.elaborator init.io
 open lean
 open lean.parser
 open lean.expander
+open lean.elaborator
 
 def check_reprint (p : list module_parser_output) (s : string) : except_t string io unit :=
 let stx := syntax.node ⟨none, p.map (λ o, o.cmd)⟩ in
@@ -89,9 +90,11 @@ universes u v
 #eval (do {
   s ← io.fs.read_file "../../library/init/core.lean",
   let s := (s.mk_iterator.nextn 6500).prev_to_string,
-  cfg ← monad_except.lift_except $ mk_config,
-  let k := parser.run cfg s (λ _, module.parser),
-  outs ← io.prim.iterate_eio (k, cfg, ([] : list module_parser_output)) $ λ ⟨k, cfg, outs⟩, match k.resume cfg with
+  parser_cfg ← monad_except.lift_except $ mk_config,
+  let cfg : elaborator_config := {filename := "foo"},
+  let st : elaborator_state := {parser_cfg := {..parser_cfg}},
+  let k := parser.run parser_cfg s (λ _, module.parser),
+  outs ← io.prim.iterate_eio (k, st, ([] : list module_parser_output)) $ λ ⟨k, st, outs⟩, match k.resume st.parser_cfg with
     | coroutine_result_core.done p := pure (sum.inr outs.reverse)
     | coroutine_result_core.yielded out k := do {
       match out.messages.to_list with
@@ -103,8 +106,14 @@ universes u v
         io.println "partial syntax tree:",
         io.println (to_string out.cmd)-/
       },
+      --io.println out.cmd,
       match (expand out.cmd).run {filename := "init/core.lean"} with
-      | except.ok cmd' := pure (sum.inl (k, out.cfg, out :: outs))
+      | except.ok cmd' := do {
+        --io.println cmd',
+        match ((elaborate cmd').run cfg).run {st with parser_cfg := out.cfg} with
+        | except.ok ((), st) := pure (sum.inl (k, st, out :: outs))
+        | except.error e := throw e.text
+      }
       | except.error e := throw e.text
     },
   check_reprint outs s,
diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out
index ce1b13337a..9fddcddb3e 100644
--- a/tests/lean/parser1.lean.expected.out
+++ b/tests/lean/parser1.lean.expected.out
@@ -106,2321 +106,6 @@ result:
    (term.ident `v [])))
  (eoi "")]
 (ok "notationa`+`:65 b:65 :=nat.addab")
+parser1.lean:90:0: error: register_notation: unreachable
 error at line 221, column 6:
 unexpected '='
-error at line 223, column 44:
-unexpected '='
-expected ":=", "." or "|"
-error at line 226, column 63:
-unexpected '='
-expected ")"
-error at line 229, column 12:
-unexpected '▸'
-expected ":="
-result:
-[(module.header [(module.prelude "prelude")] [])
- (command.notation
-  "notation"
-  (command.notation_spec
-   []
-   [(command.notation_spec.rule
-     (command.notation_spec.notation_symbol
-      (0 (command.notation_spec.notation_quoted_symbol "`" "Prop" "`" [])))
-     [])])
-  ":="
-  (term.sort_app (term.sort (0 "Sort")) (level.leading (4 (number (0 "0"))))))
- (command.notation
-  "notation"
-  (command.notation_spec
-   [`f]
-   [(command.notation_spec.rule
-     (command.notation_spec.notation_symbol
-      (0
-       (command.notation_spec.notation_quoted_symbol
-        "`"
-        " $ "
-        "`"
-        [(command.notation_spec.precedence ":" (number (0 "1")))])))
-     [(command.notation_spec.transition
-       (2
-        (command.notation_spec.argument
-         `a
-         [(command.notation_spec.action
-           ":"
-           (command.notation_spec.action_kind (0 (number (0 "0")))))])))])])
-  ":="
-  (term.app (term.ident `f []) (term.ident `a [])))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (0 "prefix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     "¬"
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "40")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (0 "prefix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     "~"
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "40")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∧ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "35")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " /\\ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "35")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " \\/ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "30")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∨ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "30")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " <-> "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "20")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ↔ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "20")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " = "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " == "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ≠ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ≈ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ~ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ≡ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ⬝ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "75")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ▸ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "75")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ▹ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "75")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ⊕ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "30")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " × "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "35")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " + "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "65")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " - "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "65")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " * "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "70")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " / "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "70")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " % "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "70")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " %ₙ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "70")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (0 "prefix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     "-"
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "100")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ^ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "80")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∘ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "90")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " <= "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ≤ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " < "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " >= "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ≥ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " > "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (0 "prefix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     "!"
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "40")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " && "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "35")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " || "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "30")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∈ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∉ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∩ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "70")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∪ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "65")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ⊆ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ⊇ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ⊂ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ⊃ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " \\ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "70")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (1 "infix"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ∣ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "50")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " ++ "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "65")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (3 "infixr"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     " :: "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "67")))]))))
- (command.reserve_mixfix
-  ["reserve" (command.mixfix.kind (2 "infixl"))]
-  (command.notation_spec.notation_symbol
-   (0
-    (command.notation_spec.notation_quoted_symbol
-     "`"
-     "; "
-     "`"
-     [(command.notation_spec.precedence ":" (number (0 "1")))]))))
- (command.universes "universes" [`u `v `w])
- (command.declaration
-  (command.decl_modifiers
-   ["/-- Auxiliary meta constant used by the compiler when erasing proofs from code. -/"]
-   []
-   []
-   ["meta"]
-   [])
-  (command.declaration.inner
-   (5
-    (command.constant
-     "constant"
-     (term.ident `lc_proof [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type ":" (term.ident `Prop []))]
-           [])
-          "}")))]
-      [(command.decl_type ":" (term.ident `α []))])))))
- (command.declaration
-  (command.decl_modifiers
-   ["/-- Auxiliary meta constant used by the compiler to mark unreachable code. -/"]
-   []
-   []
-   ["meta"]
-   [])
-  (command.declaration.inner
-   (5
-    (command.constant
-     "constant"
-     (term.ident `lc_unreachable [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-           [])
-          "}")))]
-      [(command.decl_type ":" (term.ident `α []))])))))
- (command.declaration
-  (command.decl_modifiers
-   ["/-- Auxiliary meta constant used by the compiler to mark type casting. -/"]
-   []
-   []
-   ["meta"]
-   [])
-  (command.declaration.inner
-   (5
-    (command.constant
-     "constant"
-     (term.ident `lc_cast [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `β [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `v))))]
-           [])
-          "}")))]
-      [(command.decl_type ":" (term.arrow (term.ident `α []) "→" (term.ident `β [])))])))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `inline [])] "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `id [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `α []))])
-     (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a []))))))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `inline [])] "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `flip [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `β [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `v))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `φ [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `w))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `f [])))]
-             [(term.binder_content_type
-               ":"
-               (term.arrow
-                (term.ident `α [])
-                "→"
-                (term.arrow (term.ident `β []) "→" (term.ident `φ []))))]
-             [])))
-          ")")))]
-      [(command.decl_type
-        ":"
-        (term.arrow
-         (term.ident `β [])
-         "→"
-         (term.arrow (term.ident `α []) "→" (term.ident `φ []))))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.lambda
-         "λ"
-         (term.binders
-          (1
-           (term.binder_content
-            [(term.binder_id (0 (term.ident `b [])))
-             (term.binder_id (0 (term.ident `a [])))]
-            []
-            [])))
-         ","
-         (term.app (term.app (term.ident `f []) (term.ident `a [])) (term.ident `b []))))))))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `inline [])] "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `id_delta [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `α []))])
-     (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a []))))))))
- (command.declaration
-  (command.decl_modifiers
-   ["/-- Gadget for optional parameter support. -/"]
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `reducible [])] "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `opt_param [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `default [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type
-        ":"
-        (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))])
-     (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `α []))))))))
- (command.declaration
-  (command.decl_modifiers
-   ["/-- Gadget for marking output parameters in type classes. -/"]
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `reducible [])] "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `out_param [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-             [])))
-          ")")))]
-      [(command.decl_type
-        ":"
-        (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))])
-     (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `α []))))))))
- (command.declaration
-  (command.decl_modifiers
-   ["/-- Auxiliary declaration used to implement the notation (a : α) -/"]
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `reducible [])] "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `typed_expr [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `α []))])
-     (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a []))))))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `macro_inline [])] "]")])
-  (command.declaration.inner
-   (1
-    (command.abbreviation
-     "abbreviation"
-     (term.ident `id_rhs [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `α []))])
-     (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `a []))))))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (7
-    (command.inductive
-     "inductive"
-     (term.ident `punit [])
-     (command.decl_sig
-      []
-      [(command.decl_type
-        ":"
-        (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))])
-     []
-     [(command.intro_rule
-       "|"
-       `star
-       []
-       (command.decl_sig [] [(command.decl_type ":" (term.ident `punit []))]))]))))
- (command.declaration
-  (command.decl_modifiers
-   ["/-- An abbreviation for `punit.{0}`, its most common instantiation.\n    This type should be preferred over `punit` where possible to avoid\n    unnecessary universe parameters. -/"]
-   []
-   []
-   []
-   [])
-  (command.declaration.inner
-   (1
-    (command.abbreviation
-     "abbreviation"
-     (term.ident `unit [])
-     (command.decl_sig [] [(command.decl_type ":" (term.sort (1 "Type")))])
-     (command.decl_val (0 (command.simple_decl_val ":=" (term.ident `punit []))))))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `pattern [])] "]")])
-  (command.declaration.inner
-   (1
-    (command.abbreviation
-     "abbreviation"
-     (term.ident `unit.star [])
-     (command.decl_sig [] [(command.decl_type ":" (term.ident `unit []))])
-     (command.decl_val
-      (0 (command.simple_decl_val ":=" (term.ident `punit.star []))))))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (8
-    (command.structure
-     "structure"
-     (term.ident `thunk [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-             [])))
-          ")")))]
-      [(command.decl_type
-        ":"
-        (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))])
-     []
-     ":="
-     []
-     [(command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `fn [])))]
-              [(term.binder_content_type
-                ":"
-                (term.arrow (term.ident `unit []) "→" (term.ident `α [])))]
-              [])))
-           ")")))))]))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `thunk.pure [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `thunk []) (term.ident `α [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.anonymous_constructor
-         "⟨"
-         [(term.lambda
-           "λ"
-           (term.binders
-            (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))
-           ","
-           (term.ident `a []))]
-         "⟩"))))))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `thunk.get [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `x [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.ident `thunk []) (term.ident `α [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `α []))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.app (term.ident `x.fn []) (term.paren "(" [] ")")))))))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `thunk.map [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `β [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `f [])))]
-             [(term.binder_content_type
-               ":"
-               (term.arrow (term.ident `α []) "→" (term.ident `β [])))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `x [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.ident `thunk []) (term.ident `α [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `thunk []) (term.ident `β [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.anonymous_constructor
-         "⟨"
-         [(term.lambda
-           "λ"
-           (term.binders
-            (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))
-           ","
-           (term.app (term.ident `f []) (term.ident `x.get [])))]
-         "⟩"))))))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `thunk.bind [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `β [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `x [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.ident `thunk []) (term.ident `α [])))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `f [])))]
-             [(term.binder_content_type
-               ":"
-               (term.arrow
-                (term.ident `α [])
-                "→"
-                (term.app (term.ident `thunk []) (term.ident `β []))))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `thunk []) (term.ident `β [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.anonymous_constructor
-         "⟨"
-         [(term.lambda
-           "λ"
-           (term.binders
-            (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))
-           ","
-           (term.projection
-            (term.paren "(" [(term.app (term.ident `f []) (term.ident `x.get []))] ")")
-            "."
-            (term.projection_spec (0 `get))))]
-         "⟩"))))))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (8
-    (command.structure
-     "structure"
-     (term.ident `task [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-             [])))
-          ")")))]
-      [(command.decl_type
-        ":"
-        (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))])
-     []
-     ":="
-     []
-     [(command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `fn [])))]
-              [(term.binder_content_type
-                ":"
-                (term.arrow (term.ident `unit []) "→" (term.ident `α [])))]
-              [])))
-           ")")))))]))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `task.pure [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `task []) (term.ident `α [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.anonymous_constructor
-         "⟨"
-         [(term.lambda
-           "λ"
-           (term.binders
-            (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))
-           ","
-           (term.ident `a []))]
-         "⟩"))))))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `task.get [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `x [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.ident `task []) (term.ident `α [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `α []))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.app (term.ident `x.fn []) (term.paren "(" [] ")")))))))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `task.map [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `β [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `f [])))]
-             [(term.binder_content_type
-               ":"
-               (term.arrow (term.ident `α []) "→" (term.ident `β [])))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `x [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.ident `task []) (term.ident `α [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `task []) (term.ident `β [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.anonymous_constructor
-         "⟨"
-         [(term.lambda
-           "λ"
-           (term.binders
-            (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))
-           ","
-           (term.app (term.ident `f []) (term.ident `x.get [])))]
-         "⟩"))))))))
- (command.declaration
-  (command.decl_modifiers [] [(command.visibility (1 "protected"))] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `task.bind [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `β [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `x [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.ident `task []) (term.ident `α [])))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `f [])))]
-             [(term.binder_content_type
-               ":"
-               (term.arrow
-                (term.ident `α [])
-                "→"
-                (term.app (term.ident `task []) (term.ident `β []))))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `task []) (term.ident `β [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.anonymous_constructor
-         "⟨"
-         [(term.lambda
-           "λ"
-           (term.binders
-            (1 (term.binder_content [(term.binder_id (1 (term.hole "_")))] [] [])))
-           ","
-           (term.projection
-            (term.paren "(" [(term.app (term.ident `f []) (term.ident `x.get []))] ")")
-            "."
-            (term.projection_spec (0 `get))))]
-         "⟩"))))))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (7
-    (command.inductive
-     "inductive"
-     (term.ident `true [])
-     (command.decl_sig [] [(command.decl_type ":" (term.ident `Prop []))])
-     []
-     [(command.intro_rule
-       "|"
-       `intro
-       []
-       (command.decl_sig [] [(command.decl_type ":" (term.ident `true []))]))]))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (7
-    (command.inductive
-     "inductive"
-     (term.ident `false [])
-     (command.decl_sig [] [(command.decl_type ":" (term.ident `Prop []))])
-     []
-     []))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (7
-    (command.inductive
-     "inductive"
-     (term.ident `empty [])
-     (command.decl_sig [] [(command.decl_type ":" (term.sort (1 "Type")))])
-     []
-     []))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `not [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `Prop []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `Prop []))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.arrow (term.ident `a []) "→" (term.ident `false [])))))))))
- (command.mixfix
-  (command.mixfix.kind (0 "prefix"))
-  (command.notation_spec.notation_symbol
-   (0 (command.notation_spec.notation_quoted_symbol "`" "¬" "`" [])))
-  ":="
-  (term.ident `not []))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (7
-    (command.inductive
-     "inductive"
-     (term.ident `eq [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type
-        ":"
-        (term.arrow (term.ident `α []) "→" (term.ident `Prop [])))])
-     []
-     [(command.intro_rule
-       "|"
-       `refl
-       []
-       (command.decl_sig
-        []
-        [(command.decl_type ":" (term.app (term.ident `eq []) (term.ident `a [])))]))]))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute
-     "@["
-     [(command.attr_instance `elab_as_eliminator [])
-      ","
-      (command.attr_instance `inline [])
-      ","
-      (command.attr_instance `reducible [])]
-     "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     [(command.old_univ_params "{" [`u1 `u2] "}")]
-     (term.ident `eq.ndrec [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u2))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `a [])))]
-           [(term.binder_content_type ":" (term.ident `α []))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `C [])))]
-           [(term.binder_content_type
-             ":"
-             (term.arrow
-              (term.ident `α [])
-              "→"
-              (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u1)))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `m [])))]
-             [(term.binder_content_type ":" (term.app (term.ident `C []) (term.ident `a [])))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `b [])))]
-           [(term.binder_content_type ":" (term.ident `α []))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `h [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.app (term.ident `eq []) (term.ident `a [])) (term.ident `b [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `C []) (term.ident `b [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.app
-         (term.app
-          (term.app
-           (term.app
-            (term.app
-             (term.app
-              (term.explicit (term.explicit_modifier (0 "@")) (term.ident `eq.rec []))
-              (term.ident `α []))
-             (term.ident `a []))
-            (term.paren
-             "("
-             [(term.lambda
-               "λ"
-               (term.binders
-                (1
-                 (term.binder_content
-                  [(term.binder_id (0 (term.ident `α []))) (term.binder_id (1 (term.hole "_")))]
-                  []
-                  [])))
-               ","
-               (term.app (term.ident `C []) (term.ident `α [])))]
-             ")"))
-           (term.ident `m []))
-          (term.ident `b []))
-         (term.ident `h [])))))))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute
-     "@["
-     [(command.attr_instance `elab_as_eliminator [])
-      ","
-      (command.attr_instance `inline [])
-      ","
-      (command.attr_instance `reducible [])]
-     "]")])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     [(command.old_univ_params "{" [`u1 `u2] "}")]
-     (term.ident `eq.ndrec_on [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u2))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `a [])))]
-           [(term.binder_content_type ":" (term.ident `α []))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `C [])))]
-           [(term.binder_content_type
-             ":"
-             (term.arrow
-              (term.ident `α [])
-              "→"
-              (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u1)))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `b [])))]
-           [(term.binder_content_type ":" (term.ident `α []))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `h [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.app (term.ident `eq []) (term.ident `a [])) (term.ident `b [])))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `m [])))]
-             [(term.binder_content_type ":" (term.app (term.ident `C []) (term.ident `a [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.app (term.ident `C []) (term.ident `b [])))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.app
-         (term.app
-          (term.app
-           (term.app
-            (term.app
-             (term.app
-              (term.app
-               (term.explicit (term.explicit_modifier (0 "@")) (term.ident `eq.rec []))
-               (term.ident `α []))
-              (term.ident `a []))
-             (term.paren
-              "("
-              [(term.lambda
-                "λ"
-                (term.binders
-                 (1
-                  (term.binder_content
-                   [(term.binder_id (0 (term.ident `α []))) (term.binder_id (1 (term.hole "_")))]
-                   []
-                   [])))
-                ","
-                (term.app (term.ident `C []) (term.ident `α [])))]
-              ")"))
-            (term.ident `m []))
-           (term.ident `b []))
-          (term.ident `h []))
-         (term.ident `init_quot [])))))))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (7
-    (command.inductive
-     "inductive"
-     (term.ident `heq [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `α [])))]
-           [(term.binder_content_type
-             ":"
-             (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))]
-             [(term.binder_content_type ":" (term.ident `α []))]
-             [])))
-          ")")))]
-      [(command.decl_type
-        ":"
-        (term.pi
-         "Π"
-         (term.binders
-          (0
-           [(term.bracketed_binder
-             (1
-              (term.implicit_binder
-               "{"
-               (term.binder_content
-                [(term.binder_id (0 (term.ident `β [])))]
-                [(term.binder_content_type
-                  ":"
-                  (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-                [])
-               "}")))]))
-         ","
-         (term.arrow (term.ident `β []) "→" (term.ident `Prop []))))])
-     []
-     [(command.intro_rule
-       "|"
-       `refl
-       []
-       (command.decl_sig
-        []
-        [(command.decl_type ":" (term.app (term.ident `heq []) (term.ident `a [])))]))]))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (8
-    (command.structure
-     "structure"
-     (term.ident `prod [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (1 "Type")) (level.leading (5 `u))))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `β [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (1 "Type")) (level.leading (5 `v))))]
-             [])))
-          ")")))]
-      [])
-     []
-     ":="
-     []
-     [(command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `fst [])))]
-              [(term.binder_content_type ":" (term.ident `α []))]
-              [])))
-           ")")))))
-      (command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `snd [])))]
-              [(term.binder_content_type ":" (term.ident `β []))]
-              [])))
-           ")")))))]))))
- (command.declaration
-  (command.decl_modifiers
-   ["/-- Similar to `prod`, but α and β can be propositions.\n   We use this type internally to automatically generate the brec_on recursor. -/"]
-   []
-   []
-   []
-   [])
-  (command.declaration.inner
-   (8
-    (command.structure
-     "structure"
-     (term.ident `pprod [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `α [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-             [])))
-          ")")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `β [])))]
-             [(term.binder_content_type
-               ":"
-               (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `v))))]
-             [])))
-          ")")))]
-      [])
-     []
-     ":="
-     []
-     [(command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `fst [])))]
-              [(term.binder_content_type ":" (term.ident `α []))]
-              [])))
-           ")")))))
-      (command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `snd [])))]
-              [(term.binder_content_type ":" (term.ident `β []))]
-              [])))
-           ")")))))]))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (8
-    (command.structure
-     "structure"
-     (term.ident `and [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))
-              (term.binder_id (0 (term.ident `b [])))]
-             [(term.binder_content_type ":" (term.ident `Prop []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `Prop []))])
-     []
-     ":="
-     [(command.structure_ctor `intro [] "::")]
-     [(command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `left [])))]
-              [(term.binder_content_type ":" (term.ident `a []))]
-              [])))
-           ")")))))
-      (command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `right [])))]
-              [(term.binder_content_type ":" (term.ident `b []))]
-              [])))
-           ")")))))]))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `and.elim_left [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `a [])))
-            (term.binder_id (0 (term.ident `b [])))]
-           [(term.binder_content_type ":" (term.ident `Prop []))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `h [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.app (term.ident `and []) (term.ident `a [])) (term.ident `b [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `a []))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.projection
-         (term.ident `h [])
-         "."
-         (term.projection_spec (1 (number (0 "1"))))))))))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (0
-    (command.def
-     "def"
-     []
-     (term.ident `and.elim_right [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (1
-         (term.implicit_binder
-          "{"
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `a [])))
-            (term.binder_id (0 (term.ident `b [])))]
-           [(term.binder_content_type ":" (term.ident `Prop []))]
-           [])
-          "}")))
-       (term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `h [])))]
-             [(term.binder_content_type
-               ":"
-               (term.app (term.app (term.ident `and []) (term.ident `a [])) (term.ident `b [])))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `b []))])
-     (command.decl_val
-      (0
-       (command.simple_decl_val
-        ":="
-        (term.projection
-         (term.ident `h [])
-         "."
-         (term.projection_spec (1 (number (0 "2"))))))))))))
- (command.declaration
-  (command.decl_modifiers [] [] [] [] [])
-  (command.declaration.inner
-   (8
-    (command.structure
-     "structure"
-     (term.ident `iff [])
-     (command.decl_sig
-      [(term.bracketed_binder
-        (0
-         (term.explicit_binder
-          "("
-          (term.explicit_binder_content
-           (1
-            (term.binder_content
-             [(term.binder_id (0 (term.ident `a [])))
-              (term.binder_id (0 (term.ident `b [])))]
-             [(term.binder_content_type ":" (term.ident `Prop []))]
-             [])))
-          ")")))]
-      [(command.decl_type ":" (term.ident `Prop []))])
-     []
-     ":="
-     [(command.structure_ctor `intro [] "::")]
-     [(command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `mp [])))]
-              [(term.binder_content_type
-                ":"
-                (term.arrow (term.ident `a []) "→" (term.ident `b [])))]
-              [])))
-           ")")))))
-      (command.structure_field
-       (1
-        (term.bracketed_binder
-         (0
-          (term.explicit_binder
-           "("
-           (term.explicit_binder_content
-            (1
-             (term.binder_content
-              [(term.binder_id (0 (term.ident `mpr [])))]
-              [(term.binder_content_type
-                ":"
-                (term.arrow (term.ident `b []) "→" (term.ident `a [])))]
-              [])))
-           ")")))))]))))
- (command.mixfix
-  (command.mixfix.kind (1 "infix"))
-  (command.notation_spec.notation_symbol
-   (command.notation_spec.notation_quoted_symbol
-    <missing>
-    <missing>
-    <missing>
-    <missing>))
-  <missing>
-  <missing>)
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute "@[" [(command.attr_instance `pattern [])] "]")])
-  (command.declaration.inner
-   (command.def
-    "def"
-    []
-    (term.ident `rfl [])
-    (command.decl_sig
-     [(term.bracketed_binder
-       (1
-        (term.implicit_binder
-         "{"
-         (term.binder_content
-          [(term.binder_id (0 (term.ident `α [])))]
-          [(term.binder_content_type
-            ":"
-            (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-          [])
-         "}")))
-      (term.bracketed_binder
-       (1
-        (term.implicit_binder
-         "{"
-         (term.binder_content
-          [(term.binder_id (0 (term.ident `a [])))]
-          [(term.binder_content_type ":" (term.ident `α []))]
-          [])
-         "}")))]
-     [(command.decl_type ":" (term.ident `a []))])
-    (command.decl_val (command.simple_decl_val <missing> <missing>)))))
- (command.declaration
-  (command.decl_modifiers
-   []
-   []
-   []
-   []
-   [(command.decl_attribute
-     "@["
-     [(command.attr_instance `elab_as_eliminator [])]
-     "]")])
-  (command.declaration.inner
-   (command.theorem
-    "theorem"
-    (term.ident `eq.subst [])
-    (command.decl_sig
-     [(term.bracketed_binder
-       (1
-        (term.implicit_binder
-         "{"
-         (term.binder_content
-          [(term.binder_id (0 (term.ident `α [])))]
-          [(term.binder_content_type
-            ":"
-            (term.sort_app (term.sort (0 "Sort")) (level.leading (5 `u))))]
-          [])
-         "}")))
-      (term.bracketed_binder
-       (1
-        (term.implicit_binder
-         "{"
-         (term.binder_content
-          [(term.binder_id (0 (term.ident `P [])))]
-          [(term.binder_content_type
-            ":"
-            (term.arrow (term.ident `α []) "→" (term.ident `Prop [])))]
-          [])
-         "}")))
-      (term.bracketed_binder
-       (1
-        (term.implicit_binder
-         "{"
-         (term.binder_content
-          [(term.binder_id (0 (term.ident `a [])))
-           (term.binder_id (0 (term.ident `b [])))]
-          [(term.binder_content_type ":" (term.ident `α []))]
-          [])
-         "}")))
-      (term.bracketed_binder
-       (term.explicit_binder
-        "("
-        (term.explicit_binder_content
-         (1
-          (term.binder_content
-           [(term.binder_id (0 (term.ident `h₁ [])))]
-           [(term.binder_content_type ":" (term.ident `a []))]
-           [])))
-        <missing>))
-      <missing>]
-     <missing>)
-    <missing>)))
- (command.notation
-  "notation"
-  (command.notation_spec [`h1] [])
-  <missing>
-  <missing>)
- (eoi "")]