auto fix files - sonnet

2024-08-16 16:10:27 +03:00 · 2024-07-05 13:00:18 -03:00 · 2024-07-05 13:00:18 -03:00 · e20170a8bb
commit e20170a8bb
parent d409b9d5b7
264 changed files with 10034 additions and 3956 deletions
--- a/book/Bool/lemma/double_negation.kind2
+++ b/book/Bool/lemma/double_negation.kind2
@ -2,6 +2,6 @@ use Bool/{true,false,not}

 double_negation (x: Bool) : (Equal Bool (not (not x)) x) =
  match x {
-    true : {=}
-    false: {=}
+    true: (Equal/refl/ Bool/true)
+    false: (Equal/refl/ Bool/false)
  }
--- a/book/Char/escapes.kind2
+++ b/book/Char/escapes.kind2
@ -1,15 +1,13 @@
-use Pair/{new}
-
 escapes : (List (Pair Char Char)) =
  [
-    (new 98 8)
-    (new 102 12)
-    (new 110 10)
-    (new 114 13)
-    (new 116 9)
-    (new 118 11)
-    (new 92 92)
-    (new 34 34)
-    (new 48 0)
-    (new 39 39)
+    (Pair/new _ _ 98 8)
+    (Pair/new _ _ 102 12)
+    (Pair/new _ _ 110 10)
+    (Pair/new _ _ 114 13)
+    (Pair/new _ _ 116 9)
+    (Pair/new _ _ 118 11)
+    (Pair/new _ _ 92 92)
+    (Pair/new _ _ 34 34)
+    (Pair/new _ _ 48 0)
+    (Pair/new _ _ 39 39)
  ]
--- a/book/Cmp/is_gtn.kind2
+++ b/book/Cmp/is_gtn.kind2
@ -1,8 +1,8 @@
 use Bool/{true,false}
 use Cmp/{ltn,eql,gtn}

-Cmp.is_gtn (cmp: Cmp) : Bool =
-  match cmp {
+Cmp/is_gtn (cmp: Cmp) : Bool
+  = match cmp {
    ltn: false
    eql: false
    gtn: true
--- a/book/Cmp/match.kind2
+++ b/book/Cmp/match.kind2
@ -0,0 +1,8 @@
+Cmp/match
+  (P: Cmp -> *)
+  (l: (P Cmp/ltn))
+  (e: (P Cmp/eql))
+  (g: (P Cmp/gtn))
+  (c: Cmp)
+: (P c) =
+  (~c P l e g)
--- a/book/Equal/apply.kind2
+++ b/book/Equal/apply.kind2
@ -1,20 +1,4 @@
 apply <A: *> <B: *> <a: A> <b: B> (f: A -> B) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
  match e {
-    Equal/refl: ~λPλrefl(refl (f e.a))
+    Equal/refl: ~λPλe(e (f e.a))
  }: (Equal B (f a) (f b))
-
-  //(Equal/match
-    //λaλbλe(Equal B (f a) (f b))
-    //λx ~λPλrefl(refl (f x))
-    //e)
-
-//Equal.apply
-//: ∀(A: *)
-  //∀(B: *)
-  //∀(f: ∀(x: A) B)
-  //∀(a: A)
-  //∀(b: A)
-  //∀(e: (Equal A a b))
-  //(Equal B (f a) (f b))
-//= λA λB λf λa λb λe
-  //(e λx (Equal B (f a) (f x)) λP λx x)
--- a/book/Equal/match.kind2
+++ b/book/Equal/match.kind2
@ -1,6 +1,6 @@
 match <T: *> <a: T> <b: T> 
  (P: ∀(a:T) ∀(b:T) ∀(e: (Equal T a b)) *)
-  (refl: ∀(x: T) (P x x (Equal/refl/ T x)))
+  (refl: ∀(x: T) (P x x (Equal/refl T x)))
  (e: (Equal T a b))
 : (P a b e) =
  (~e P refl)
--- a/book/IO/_.kind2
+++ b/book/IO/_.kind2
@ -1,18 +1,16 @@
-data IO A
+data IO <A>
 | print (text: String) (then: ∀(x: Unit) (IO A))
 | load (file: String) (then: ∀(x: String) (IO A))
 | save (file: String) (text: String) (then: ∀(x: Unit) (IO A))
 | done (term: A)

-
-
 //IO
 //: ∀(A: *) *
 //= λA
-  //$(self: (IO A))
-  //∀(P: ∀(x: (IO A)) *)
-  //∀(print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.print A text then)))
-  //∀(load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO.load A file then)))
-  //∀(save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file text then)))
-  //∀(done: ∀(term: A) (P (IO.done A term)))
-  //(P self)
+//  $(self: (IO A))
+//  ∀(P: ∀(x: (IO A)) *)
+//  ∀(print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/print A text then)))
+//  ∀(load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO/load A file then)))
+//  ∀(save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/save A file text then)))
+//  ∀(done: ∀(term: A) (P (IO/done A term)))
+//  (P self)
--- a/book/IO/bind.kind2
+++ b/book/IO/bind.kind2
@ -1,14 +1,12 @@
 bind <A> <B> (a: (IO A)) (b: A -> (IO B)) : (IO B) =
  match a {
-    IO/print: (IO/print B a.text λx (IO/bind (a.then x) b))
-    IO/load: (IO/load B a.file λs (IO/bind (a.then s) b))
-    IO/save: (IO/save B a.file a.text λx (IO/bind (a.then Unit/new) b))
+    IO/print: (IO/print B a.text λx (IO/bind A B (a.then x) b))
+    IO/load: (IO/load B a.file λs (IO/bind A B (a.then s) b))
+    IO/save: (IO/save B a.file a.text λx (IO/bind A B (a.then Unit/new) b))
    IO/done: (b a.term)
  }

-
-
-//IO.bind
+//IO/bind
 //: ∀(A: *)
  //∀(B: *)
  //∀(a: (IO A))
@ -17,15 +15,15 @@ bind <A> <B> (a: (IO A)) (b: A -> (IO B)) : (IO B) =
 //= λA λB λa λb
  //use P = λx ∀(b: ∀(x: A) (IO B)) (IO B)
  //use print = λtext λthen λb
-    //(IO.print B text λx (IO.bind A B (then x) b))
+    //(IO/print B text λx (IO/bind A B (then x) b))
  //use load = λfile λthen λb
-    //(IO.load B file λs (IO.bind A B (then s) b))
+    //(IO/load B file λs (IO/bind A B (then s) b))
  //use save = λfile λdata λthen λb
-    //(IO.save
+    //(IO/save
      //B
      //file
      //data
-      //λx (IO.bind A B (then Unit.one) b)
+      //λx (IO/bind A B (then Unit/one) b)
    //)
  //use done = λterm λb (b term)
  //(~a P print load save done b)
--- a/book/IO/done.kind2
+++ b/book/IO/done.kind2
@ -1,3 +1,3 @@
-IO.done
+IO/done
 : ∀(A: *) ∀(term: A) (IO A)
 = λA λterm ~λP λprint λload λsave λdone (done term)
--- a/book/IO/load.kind2
+++ b/book/IO/load.kind2
@ -1,4 +1,4 @@
-IO.load
+IO/load
 : ∀(A: *)
  ∀(file: String)
  ∀(then: ∀(x: String) (IO A))
--- a/book/IO/match.kind2
+++ b/book/IO/match.kind2
@ -0,0 +1,9 @@
+match <A> <B>
+  (P: (IO A) -> *)
+  (print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/print A text then)))
+  (load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO/load A file then)))
+  (save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO/save A file text then)))
+  (done: ∀(term: A) (P (IO/done A term)))
+  (x: (IO A))
+: (P x) =
+  (~x P print load save done)
--- a/book/IO/print.kind2
+++ b/book/IO/print.kind2
@ -1,4 +1,4 @@
-IO.print
+IO/print
 : ∀(A: *) ∀(text: String) ∀(then: ∀(x: Unit) (IO A))
  (IO A)
 = λA λtext λthen
--- a/book/IO/run.kind2
+++ b/book/IO/run.kind2
@ -1,22 +1,20 @@
 run <A> (x: (IO A)) : (IO A) =
  match x {
-    IO/print: (HVM/print x.text (run (x.then Unit/new)))
-    IO/load: (HVM/load x.file λs (IO/run (x.then s)))
-    IO/save: (HVM/save x.file x.text (IO/run (x.then Unit/new)))
+    IO/print: (IO/print A x.text λu (run A (x.then Unit/new)))
+    IO/load: (IO/load A x.file λs (run A (x.then s)))
+    IO/save: (IO/save A x.file x.text λu (run A (x.then Unit/new)))
    IO/done: (IO/done A x.term)
  }

-
-
-//IO.run
+//IO/run
 //: ∀(A: *) ∀(x: (IO A)) (IO A)
 //= λA λx
  //use P = λx (IO A)
  //use print = λtext λthen
-    //(HVM.print (IO A) text (IO.run A (then Unit.one)))
+    //(IO/print A text λu (IO/run A (then Unit/new)))
  //use load = λfile λthen
-    //(HVM.load (IO A) file λs (IO.run A (then s)))
+    //(IO/load A file λs (IO/run A (then s)))
  //use save = λfile λtext λthen
-    //(HVM.save (IO A) file text (IO.run A (then Unit.one)))
-  //use done = λterm (IO.done A term)
+    //(IO/save A file text λu (IO/run A (then Unit/new)))
+  //use done = λterm (IO/done A term)
  //(~x P print load save done)
--- a/book/IO/save.kind2
+++ b/book/IO/save.kind2
@ -1,4 +1,4 @@
-IO.save
+IO/save
 : ∀(A: *)
  ∀(file: String)
  ∀(text: String)
--- a/book/Kind/API/check.kind2
+++ b/book/Kind/API/check.kind2
@ -1,19 +0,0 @@
-Kind.API.check
-: ∀(term: Kind.Term) (IO Unit)
-= λterm
-  (IO.run
-    Unit
-    (Kind.if.ref
-      term
-      (IO Unit)
-      λnam λval (Kind.API.check val)
-      λterm
-      (Kind.if.ann
-        term
-        (IO Unit)
-        λval λtyp
-        (Kind.API.check.done (Kind.check val typ Nat.zero))
-        λterm (Kind.API.check.done (Kind.infer term Nat.zero))
-      )
-    )
-  )
--- a/book/Kind/API/check/done.kind2
+++ b/book/Kind/API/check/done.kind2
@ -1,7 +0,0 @@
-Kind.API.check.done
-: ∀(result: (Maybe Kind.Term)) (IO Unit)
-= λresult
-  use P = λx (IO Unit)
-  use some = λvalue (IO.print.do "check")
-  use none = (IO.print.do "error")
-  (~result P some none)
--- a/book/Kind/API/get_refs.kind2
+++ b/book/Kind/API/get_refs.kind2
@ -1,20 +0,0 @@
-Kind.API.get_refs
-: ∀(name: String) (IO Unit)
-= λname
-  (IO.run
-    Unit
-    (IO.bind
-      Kind.Book
-      Unit
-      (Kind.load.code name)
-      λbook
-      (IO.bind
-        Unit
-        Unit
-        (IO.print.do
-          (String.join String.newline (Kind.Book.get_refs book))
-        )
-        λx (IO.done Unit Unit.one)
-      )
-    )
-  )
--- a/book/Kind/API/normal.kind2
+++ b/book/Kind/API/normal.kind2
@ -1,29 +0,0 @@
-Kind.API.normal
-: ∀(term: Kind.Term) (IO Unit)
-= λterm
-  (IO.run
-    Unit
-    (Kind.if.ref
-      term
-      (IO Unit)
-      λnam λval (Kind.API.normal val)
-      λterm
-      (Kind.if.ann
-        term
-        (IO Unit)
-        λval λtyp (Kind.API.normal val)
-        λterm
-        (IO.bind
-          Unit
-          Unit
-          (IO.print.do
-            (Kind.Term.show
-              (Kind.normal Bool.true term Nat.zero)
-              Nat.zero
-            )
-          )
-          λx (IO.done Unit Unit.one)
-        )
-      )
-    )
-  )
--- a/book/Kind/Binder.kind2
+++ b/book/Kind/Binder.kind2
@ -1,3 +0,0 @@
-Kind.Binder
-: *
-= (Pair String Kind.Term)
--- a/book/Kind/Binder/new.kind2
+++ b/book/Kind/Binder/new.kind2
@ -1,3 +0,0 @@
-Kind.Binder.new
-: ∀(nam: String) ∀(typ: Kind.Term) Kind.Binder
-= λnam λtyp (Pair.new String Kind.Term nam typ)
--- a/book/Kind/Book.kind2
+++ b/book/Kind/Book.kind2
@ -1,3 +0,0 @@
-Kind.Book
-: *
-= (String.Map Kind.Term)
--- a/book/Kind/Book/String.kind2
+++ b/book/Kind/Book/String.kind2
@ -1,3 +0,0 @@
-Kind.Book.String
-: Kind.Term
-= (Kind.hol "TODO" (List.nil Kind.Term))
--- a/book/Kind/Book/String/cons.kind2
+++ b/book/Kind/Book/String/cons.kind2
@ -1,3 +0,0 @@
-Kind.Book.String/cons
-: Kind.Term
-= (Kind.hol "TODO" (List.nil Kind.Term))
--- a/book/Kind/Book/String/nil.kind2
+++ b/book/Kind/Book/String/nil.kind2
@ -1,3 +0,0 @@
-Kind.Book.String/nil
-: Kind.Term
-= (Kind.hol "TODO" (List.nil Kind.Term))
--- a/book/Kind/Book/get_refs.kind2
+++ b/book/Kind/Book/get_refs.kind2
@ -1,9 +0,0 @@
-Kind.Book.get_refs
-: ∀(book: Kind.Book) (List String)
-= λbook
-  (List.Chunk.build
-    String
-    (Kind.Book.get_refs.go
-      (String.Map.to_list Kind.Term book)
-    )
-  )
--- a/book/Kind/Book/get_refs/go.kind2
+++ b/book/Kind/Book/get_refs/go.kind2
@ -1,15 +0,0 @@
-Kind.Book.get_refs.go
-: ∀(book: (List (Pair String Kind.Term)))
-  (List.Chunk String)
-= λbook
-  use P = λx (List.Chunk String)
-  use cons = λhead λtail
-    use P = λx (List.Chunk String)
-    use new = λhead.fst λhead.snd λnil
-      (Kind.Term.get_refs.go
-        head.snd
-        (Kind.Book.get_refs.go tail nil)
-      )
-    (~head P new)
-  use nil = λnil nil
-  (~book P cons nil)
--- a/book/Kind/Book/parse.kind2
+++ b/book/Kind/Book/parse.kind2
@ -1,7 +0,0 @@
-Kind.Book.parse
-: ∀(code: String) Kind.Book
-= λcode
-  use P = λx Kind.Book
-  use done = λcode λbook book
-  use fail = λerror (String.Map.new Kind.Term)
-  (~(Kind.Book.parser code) P done fail)
--- a/book/Kind/Book/parser.kind2
+++ b/book/Kind/Book/parser.kind2
@ -1,94 +0,0 @@
-Kind.Book.parser
-: (Parser Kind.Book)
-= (Parser.bind
-    Bool
-    Kind.Book
-    Parser.is_eof
-    λis_eof
-    use P = λx (Parser Kind.Book)
-    use true = (Parser.pure Kind.Book (String.Map.new Kind.Term))
-    use false = (Parser.bind
-        String
-        Kind.Book
-        Parser.name
-        λnam
-        (Parser.bind
-          Bool
-          Kind.Book
-          (Parser.skip Bool (Parser.test ":"))
-          λann
-          use P = λx (Parser Kind.Book)
-          use true = (Parser.bind
-              Unit
-              Kind.Book
-              (Parser.text ":")
-              λ_
-              (Parser.bind
-                Kind.PreTerm
-                Kind.Book
-                Kind.Term.parser
-                λtyp
-                (Parser.bind
-                  Unit
-                  Kind.Book
-                  (Parser.text "=")
-                  λ_
-                  (Parser.bind
-                    Kind.PreTerm
-                    Kind.Book
-                    Kind.Term.parser
-                    λval
-                    (Parser.bind
-                      Kind.Book
-                      Kind.Book
-                      Kind.Book.parser
-                      λbook
-                      (Parser.pure
-                        Kind.Book
-                        (String.Map.set
-                          Kind.Term
-                          nam
-                          (Kind.ann
-                            (val (List.nil Kind.Binder))
-                            (typ (List.nil Kind.Binder))
-                          )
-                          book
-                        )
-                      )
-                    )
-                  )
-                )
-              )
-            )
-          use false = (Parser.bind
-              Unit
-              Kind.Book
-              (Parser.text "=")
-              λ_
-              (Parser.bind
-                Kind.PreTerm
-                Kind.Book
-                Kind.Term.parser
-                λval
-                (Parser.bind
-                  Kind.Book
-                  Kind.Book
-                  Kind.Book.parser
-                  λbook
-                  (Parser.pure
-                    Kind.Book
-                    (String.Map.set
-                      Kind.Term
-                      nam
-                      (val (List.nil Kind.Binder))
-                      book
-                    )
-                  )
-                )
-              )
-            )
-          (~ann P true false)
-        )
-      )
-    (~is_eof P true false)
-  )
--- a/book/Kind/Book/show.kind2
+++ b/book/Kind/Book/show.kind2
@ -1,6 +0,0 @@
-Kind.Book.show
-: ∀(book: Kind.Book) String
-= λbook
-  (String.Chunk.build
-    (Kind.Book.show.go (String.Map.to_list Kind.Term book))
-  )
--- a/book/Kind/Book/show/go.kind2
+++ b/book/Kind/Book/show/go.kind2
@ -1,25 +0,0 @@
-Kind.Book.show.go
-: ∀(book: (List (Pair String Kind.Term)))
-  String.Chunk
-= λbook
-  use P = λx String.Chunk
-  use cons = λhead λtail
-    use P = λx String.Chunk
-    use new = λhead.fst λhead.snd λnil
-      (Kind.Text.show.go
-        head.fst
-        (Kind.Text.show.go
-          " = "
-          (Kind.Term.show.go
-            head.snd
-            Nat.zero
-            (Kind.Text.show.go
-              String.newline
-              (Kind.Book.show.go tail nil)
-            )
-          )
-        )
-      )
-    (~head P new)
-  use nil = λnil nil
-  (~book P cons nil)
--- a/book/Kind/Oper.kind2
+++ b/book/Kind/Oper.kind2
@ -1,21 +0,0 @@
-Kind.Oper
-: *
-= $(self: Kind.Oper)
-  ∀(P: ∀(x: Kind.Oper) *)
-  ∀(add: (P Kind.Oper.add))
-  ∀(mul: (P Kind.Oper.mul))
-  ∀(sub: (P Kind.Oper.sub))
-  ∀(div: (P Kind.Oper.div))
-  ∀(mod: (P Kind.Oper.mod))
-  ∀(eq: (P Kind.Oper.eq))
-  ∀(ne: (P Kind.Oper.ne))
-  ∀(lt: (P Kind.Oper.lt))
-  ∀(gt: (P Kind.Oper.gt))
-  ∀(lte: (P Kind.Oper.lte))
-  ∀(gte: (P Kind.Oper.gte))
-  ∀(and: (P Kind.Oper.and))
-  ∀(or: (P Kind.Oper.or))
-  ∀(xor: (P Kind.Oper.xor))
-  ∀(lsh: (P Kind.Oper.lsh))
-  ∀(rsh: (P Kind.Oper.rsh))
-  (P self)
--- a/book/Kind/Oper/add.kind2
+++ b/book/Kind/Oper/add.kind2
@ -1,4 +0,0 @@
-Kind.Oper.add
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  add
--- a/book/Kind/Oper/and.kind2
+++ b/book/Kind/Oper/and.kind2
@ -1,4 +0,0 @@
-Kind.Oper.and
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  and
--- a/book/Kind/Oper/div.kind2
+++ b/book/Kind/Oper/div.kind2
@ -1,4 +0,0 @@
-Kind.Oper.div
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  div
--- a/book/Kind/Oper/eq.kind2
+++ b/book/Kind/Oper/eq.kind2
@ -1,4 +0,0 @@
-Kind.Oper.eq
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  eq
--- a/book/Kind/Oper/gt.kind2
+++ b/book/Kind/Oper/gt.kind2
@ -1,4 +0,0 @@
-Kind.Oper.gt
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  gt
--- a/book/Kind/Oper/gte.kind2
+++ b/book/Kind/Oper/gte.kind2
@ -1,4 +0,0 @@
-Kind.Oper.gte
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  gte
--- a/book/Kind/Oper/lsh.kind2
+++ b/book/Kind/Oper/lsh.kind2
@ -1,4 +0,0 @@
-Kind.Oper.lsh
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  lsh
--- a/book/Kind/Oper/lt.kind2
+++ b/book/Kind/Oper/lt.kind2
@ -1,4 +0,0 @@
-Kind.Oper.lt
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  lt
--- a/book/Kind/Oper/lte.kind2
+++ b/book/Kind/Oper/lte.kind2
@ -1,4 +0,0 @@
-Kind.Oper.lte
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  lte
--- a/book/Kind/Oper/mod.kind2
+++ b/book/Kind/Oper/mod.kind2
@ -1,4 +0,0 @@
-Kind.Oper.mod
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  mod
--- a/book/Kind/Oper/mul.kind2
+++ b/book/Kind/Oper/mul.kind2
@ -1,4 +0,0 @@
-Kind.Oper.mul
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  mul
--- a/book/Kind/Oper/ne.kind2
+++ b/book/Kind/Oper/ne.kind2
@ -1,4 +0,0 @@
-Kind.Oper.ne
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  ne
--- a/book/Kind/Oper/or.kind2
+++ b/book/Kind/Oper/or.kind2
@ -1,4 +0,0 @@
-Kind.Oper.or
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  or
--- a/book/Kind/Oper/parser.kind2
+++ b/book/Kind/Oper/parser.kind2
@ -1,66 +0,0 @@
-Kind.Oper.parser
-: (Parser Kind.Oper)
-= use TRY = (List.cons (Parser.Guard Kind.Oper))
-  use END = (List.nil (Parser.Guard Kind.Oper))
-  use OP2 = {λsym λoper
-    (Parser.Guard.text
-      Kind.Oper
-      sym
-      (Parser.bind
-        Unit
-        Kind.Oper
-        (Parser.text sym)
-        λx (Parser.pure Kind.Oper oper)
-      )
-    )
-    :∀(sym: String) ∀(oper: Kind.Oper)
-    (Parser.Guard Kind.Oper)}
-  (Parser.variant
-    Kind.Oper
-    (TRY
-      (OP2 "+" Kind.Oper.add)
-      (TRY
-        (OP2 "*" Kind.Oper.mul)
-        (TRY
-          (OP2 "-" Kind.Oper.sub)
-          (TRY
-            (OP2 "/" Kind.Oper.div)
-            (TRY
-              (OP2 "%" Kind.Oper.mod)
-              (TRY
-                (OP2 "==" Kind.Oper.eq)
-                (TRY
-                  (OP2 "!=" Kind.Oper.ne)
-                  (TRY
-                    (OP2 "<=" Kind.Oper.lte)
-                    (TRY
-                      (OP2 ">=" Kind.Oper.gte)
-                      (TRY
-                        (OP2 "<<" Kind.Oper.lsh)
-                        (TRY
-                          (OP2 ">>" Kind.Oper.rsh)
-                          (TRY
-                            (OP2 "<" Kind.Oper.lt)
-                            (TRY
-                              (OP2 ">" Kind.Oper.gt)
-                              (TRY
-                                (OP2 "&" Kind.Oper.and)
-                                (TRY
-                                  (OP2 "|" Kind.Oper.or)
-                                  (TRY (OP2 "^" Kind.Oper.xor) END)
-                                )
-                              )
-                            )
-                          )
-                        )
-                      )
-                    )
-                  )
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Oper/rsh.kind2
+++ b/book/Kind/Oper/rsh.kind2
@ -1,4 +0,0 @@
-Kind.Oper.rsh
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  rsh
--- a/book/Kind/Oper/show.kind2
+++ b/book/Kind/Oper/show.kind2
@ -1,4 +0,0 @@
-Kind.Oper.show
-: ∀(oper: Kind.Oper) String
-= λoper
-  (String.Chunk.build (Kind.Oper.show.go oper))
--- a/book/Kind/Oper/show/go.kind2
+++ b/book/Kind/Oper/show/go.kind2
@ -1,39 +0,0 @@
-Kind.Oper.show.go
-: ∀(oper: Kind.Oper) String.Chunk
-= λoper
-  use P = λX String.Chunk
-  use add = (Kind.Text.show.go "+")
-  use mul = (Kind.Text.show.go "*")
-  use sub = (Kind.Text.show.go "-")
-  use div = (Kind.Text.show.go "/")
-  use mod = (Kind.Text.show.go "%")
-  use eq = (Kind.Text.show.go "==")
-  use ne = (Kind.Text.show.go "!=")
-  use lt = (Kind.Text.show.go "<")
-  use gt = (Kind.Text.show.go ">")
-  use lte = (Kind.Text.show.go "<=")
-  use gte = (Kind.Text.show.go ">=")
-  use and = (Kind.Text.show.go "&")
-  use or = (Kind.Text.show.go "|")
-  use xor = (Kind.Text.show.go "^")
-  use lsh = (Kind.Text.show.go "<<")
-  use rsh = (Kind.Text.show.go ">>")
-  (~oper
-    P
-    add
-    mul
-    sub
-    div
-    mod
-    eq
-    ne
-    lt
-    gt
-    lte
-    gte
-    and
-    or
-    xor
-    lsh
-    rsh
-  )
--- a/book/Kind/Oper/sub.kind2
+++ b/book/Kind/Oper/sub.kind2
@ -1,4 +0,0 @@
-Kind.Oper.sub
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  sub
--- a/book/Kind/Oper/xor.kind2
+++ b/book/Kind/Oper/xor.kind2
@ -1,4 +0,0 @@
-Kind.Oper.xor
-: Kind.Oper
-= ~λP λadd λmul λsub λdiv λmod λeq λne λlt λgt λlte λgte λand λor λxor λlsh λrsh
-  xor
--- a/book/Kind/PreTerm.kind2
+++ b/book/Kind/PreTerm.kind2
@ -1,3 +0,0 @@
-Kind.PreTerm
-: *
-= ∀(ctx: Kind.Scope) Kind.Term
--- a/book/Kind/Scope.kind2
+++ b/book/Kind/Scope.kind2
@ -1,3 +0,0 @@
-Kind.Scope
-: *
-= (List Kind.Binder)
--- a/book/Kind/Scope/cons.kind2
+++ b/book/Kind/Scope/cons.kind2
@ -1,3 +0,0 @@
-Kind.Scope.cons
-: ∀(head: Kind.Binder) ∀(tail: Kind.Scope) Kind.Scope
-= (List.cons Kind.Binder)
--- a/book/Kind/Scope/extend.kind2
+++ b/book/Kind/Scope/extend.kind2
@ -1,5 +0,0 @@
-Kind.Scope.extend
-: ∀(nam: String) ∀(typ: Kind.Term) ∀(scp: Kind.Scope)
-  Kind.Scope
-= λnam λtyp λscp
-  (Kind.Scope.cons (Kind.Binder.new nam typ) scp)
--- a/book/Kind/Scope/find.kind2
+++ b/book/Kind/Scope/find.kind2
@ -1,9 +0,0 @@
-Kind.Scope.find
-: ∀(nam: String) ∀(scp: Kind.Scope) Kind.Term
-= λname λscope
-  use cond = λbnd (~bnd λx Bool λn λt (String.equal name n))
-  use found = (List.find Kind.Binder cond scope)
-  use P = λx Kind.Term
-  use some = λbnd (~bnd λx Kind.Term λn λt t)
-  use none = (Kind.ref name Kind.set)
-  (~found P some none)
--- a/book/Kind/Scope/nil.kind2
+++ b/book/Kind/Scope/nil.kind2
@ -1,3 +0,0 @@
-Kind.Scope.nil
-: Kind.Scope
-= (List.nil Kind.Binder)
--- a/book/Kind/Term.kind2
+++ b/book/Kind/Term.kind2
@ -1,61 +0,0 @@
-Kind.Term
-: *
-= $(self: Kind.Term)
-  ∀(P: ∀(x: Kind.Term) *)
-  ∀(all: 
-    ∀(nam: String)
-    ∀(inp: Kind.Term)
-    ∀(bod: ∀(x: Kind.Term) Kind.Term)
-    (P (Kind.all nam inp bod))
-  )
-  ∀(lam: 
-    ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term)
-    (P (Kind.lam nam bod))
-  )
-  ∀(app: 
-    ∀(fun: Kind.Term) ∀(arg: Kind.Term)
-    (P (Kind.app fun arg))
-  )
-  ∀(ann: 
-    ∀(val: Kind.Term) ∀(typ: Kind.Term)
-    (P (Kind.ann val typ))
-  )
-  ∀(slf: 
-    ∀(nam: String) ∀(bod: ∀(x: Kind.Term) Kind.Term)
-    (P (Kind.slf nam bod))
-  )
-  ∀(ins: ∀(val: Kind.Term) (P (Kind.ins val)))
-  ∀(ref: 
-    ∀(nam: String) ∀(val: Kind.Term)
-    (P (Kind.ref nam val))
-  )
-  ∀(def: 
-    ∀(nam: String)
-    ∀(val: Kind.Term)
-    ∀(bod: ∀(x: Kind.Term) Kind.Term)
-    (P (Kind.def nam val bod))
-  )
-  ∀(set: (P Kind.set))
-  ∀(u60: (P Kind.u60))
-  ∀(num: ∀(val: U48) (P (Kind.num val)))
-  ∀(op2: 
-    ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term)
-    (P (Kind.op2 opr fst snd))
-  )
-  ∀(mat: 
-    ∀(nam: String)
-    ∀(x: Kind.Term)
-    ∀(z: Kind.Term)
-    ∀(s: ∀(x: Kind.Term) Kind.Term)
-    ∀(p: ∀(x: Kind.Term) Kind.Term)
-    (P (Kind.mat nam x z s p))
-  )
-  ∀(txt: ∀(lit: Kind.Text) (P (Kind.txt lit)))
-  ∀(hol: 
-    ∀(nam: String) ∀(ctx: (List Kind.Term))
-    (P (Kind.hol nam ctx))
-  )
-  ∀(var: 
-    ∀(nam: String) ∀(idx: Nat) (P (Kind.var nam idx))
-  )
-  (P self)
--- a/book/Kind/Term/get_refs.kind2
+++ b/book/Kind/Term/get_refs.kind2
@ -1,7 +0,0 @@
-Kind.Term.get_refs
-: ∀(term: Kind.Term) (List String)
-= λterm
-  (List.Chunk.build
-    String
-    (Kind.Term.get_refs.go term)
-  )
--- a/book/Kind/Term/get_refs/go.kind2
+++ b/book/Kind/Term/get_refs/go.kind2
@ -1,71 +0,0 @@
-Kind.Term.get_refs.go
-: ∀(term: Kind.Term) (List.Chunk String)
-= λterm
-  use P = λx (List.Chunk String)
-  use all = λnam λinp λbod λnil
-    (Kind.Term.get_refs.go
-      inp
-      (Kind.Term.get_refs.go (bod Kind.set) nil)
-    )
-  use lam = λnam λbod λnil
-    (Kind.Term.get_refs.go (bod Kind.set) nil)
-  use app = λfun λarg λnil
-    (Kind.Term.get_refs.go
-      fun
-      (Kind.Term.get_refs.go arg nil)
-    )
-  use ann = λval λtyp λnil
-    (Kind.Term.get_refs.go
-      val
-      (Kind.Term.get_refs.go typ nil)
-    )
-  use slf = λnam λbod λnil
-    (Kind.Term.get_refs.go (bod Kind.set) nil)
-  use ins = λval λnil (Kind.Term.get_refs.go val nil)
-  use ref = λnam λval λnil (List.cons String nam nil)
-  use def = λnam λval λbod λnil
-    (Kind.Term.get_refs.go
-      val
-      (Kind.Term.get_refs.go (bod Kind.set) nil)
-    )
-  use set = λnil nil
-  use u60 = λnil nil
-  use num = λval λnil nil
-  use op2 = λopr λfst λsnd λnil
-    (Kind.Term.get_refs.go
-      fst
-      (Kind.Term.get_refs.go snd nil)
-    )
-  use mat = λnam λx λz λs λp λnil
-    (Kind.Term.get_refs.go
-      x
-      (Kind.Term.get_refs.go
-        z
-        (Kind.Term.get_refs.go
-          (s Kind.set)
-          (Kind.Term.get_refs.go (p Kind.set) nil)
-        )
-      )
-    )
-  use txt = λtext λnil nil
-  use hol = λnam λctx λnil nil
-  use var = λnam λidx λnil nil
-  (~term
-    P
-    all
-    lam
-    app
-    ann
-    slf
-    ins
-    ref
-    def
-    set
-    u60
-    num
-    op2
-    mat
-    txt
-    hol
-    var
-  )
--- a/book/Kind/Term/parse.kind2
+++ b/book/Kind/Term/parse.kind2
@ -1,7 +0,0 @@
-Kind.Term.parse
-: ∀(code: String) Kind.Term
-= λcode
-  use P = λx Kind.Term
-  use done = λcode λterm (term (List.nil Kind.Binder))
-  use fail = λerror (Kind.hol "error" (List.nil Kind.Term))
-  (~(Kind.Term.parser code) P done fail)
--- a/book/Kind/Term/parser.kind2
+++ b/book/Kind/Term/parser.kind2
@ -1,50 +0,0 @@
-Kind.Term.parser
-: (Parser Kind.PreTerm)
-= use TRY = (List.cons (Parser.Guard Kind.PreTerm))
-  use END = (List.nil (Parser.Guard Kind.PreTerm))
-  (Parser.variant
-    Kind.PreTerm
-    (TRY
-      Kind.Term.parser.all
-      (TRY
-        Kind.Term.parser.lam
-        (TRY
-          Kind.Term.parser.app
-          (TRY
-            Kind.Term.parser.ann
-            (TRY
-              Kind.Term.parser.slf
-              (TRY
-                Kind.Term.parser.ins
-                (TRY
-                  Kind.Term.parser.set
-                  (TRY
-                    Kind.Term.parser.def
-                    (TRY
-                      Kind.Term.parser.u60
-                      (TRY
-                        Kind.Term.parser.op2
-                        (TRY
-                          Kind.Term.parser.mat
-                          (TRY
-                            Kind.Term.parser.chr
-                            (TRY
-                              Kind.Term.parser.str
-                              (TRY
-                                Kind.Term.parser.num
-                                (TRY Kind.Term.parser.hol (TRY Kind.Term.parser.var END))
-                              )
-                            )
-                          )
-                        )
-                      )
-                    )
-                  )
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/all.kind2
+++ b/book/Kind/Term/parser/all.kind2
@ -1,49 +0,0 @@
-Kind.Term.parser.all
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "∀"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "∀")
-      λ_
-      (Kind.Term.parser.bind
-        Unit
-        (Parser.text "(")
-        λ_
-        (Kind.Term.parser.bind
-          String
-          Parser.name
-          λnam
-          (Kind.Term.parser.bind
-            Unit
-            (Parser.text ":")
-            λ_
-            (Kind.Term.parser.bind
-              Kind.PreTerm
-              Kind.Term.parser
-              λinp
-              (Kind.Term.parser.bind
-                Unit
-                (Parser.text ")")
-                λ_
-                (Kind.Term.parser.bind
-                  Kind.PreTerm
-                  Kind.Term.parser
-                  λbod
-                  (Kind.Term.parser.pure
-                    λscp
-                    (Kind.all
-                      nam
-                      (inp scp)
-                      λx (bod (Kind.Scope.extend nam x scp))
-                    )
-                  )
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/ann.kind2
+++ b/book/Kind/Term/parser/ann.kind2
@ -1,34 +0,0 @@
-Kind.Term.parser.ann
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "{"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "{")
-      λ_
-      (Kind.Term.parser.bind
-        Kind.PreTerm
-        Kind.Term.parser
-        λval
-        (Kind.Term.parser.bind
-          Unit
-          (Parser.text ":")
-          λ_
-          (Kind.Term.parser.bind
-            Kind.PreTerm
-            Kind.Term.parser
-            λtyp
-            (Kind.Term.parser.bind
-              Unit
-              (Parser.text "}")
-              λ_
-              (Kind.Term.parser.pure
-                λscp (Kind.ann (val scp) (typ scp))
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/app.kind2
+++ b/book/Kind/Term/parser/app.kind2
@ -1,41 +0,0 @@
-Kind.Term.parser.app
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "("
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "(")
-      λ_
-      (Kind.Term.parser.bind
-        Kind.PreTerm
-        Kind.Term.parser
-        λfun
-        (Kind.Term.parser.bind
-          (List Kind.PreTerm)
-          (Parser.until
-            Kind.PreTerm
-            (Parser.skip Bool (Parser.test ")"))
-            Kind.Term.parser
-          )
-          λterms
-          (Kind.Term.parser.bind
-            Unit
-            (Parser.text ")")
-            λ_
-            (Kind.Term.parser.pure
-              λscp
-              (List.fold
-                Kind.PreTerm
-                terms
-                ∀(fun: Kind.Term) Kind.Term
-                λarg λrec λfun (rec (Kind.app fun (arg scp)))
-                λfun fun
-                (fun scp)
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/bind.kind2
+++ b/book/Kind/Term/parser/bind.kind2
@ -1,6 +0,0 @@
-Kind.Term.parser.bind
-: ∀(A: *)
-  ∀(a: (Parser A))
-  ∀(b: ∀(x: A) (Parser Kind.PreTerm))
-  (Parser Kind.PreTerm)
-= λA (Parser.bind A Kind.PreTerm)
--- a/book/Kind/Term/parser/chr.kind2
+++ b/book/Kind/Term/parser/chr.kind2
@ -1,21 +0,0 @@
-Kind.Term.parser.chr
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "'"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "'")
-      λ_
-      (Kind.Term.parser.bind
-        U48
-        Parser.char
-        λchr
-        (Kind.Term.parser.bind
-          Unit
-          (Parser.text "'")
-          λ_ (Kind.Term.parser.pure λscp (Kind.num chr))
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/def.kind2
+++ b/book/Kind/Term/parser/def.kind2
@ -1,39 +0,0 @@
-Kind.Term.parser.def
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "use "
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "use ")
-      λ_
-      (Kind.Term.parser.bind
-        String
-        Parser.name
-        λnam
-        (Kind.Term.parser.bind
-          Unit
-          (Parser.text "=")
-          λ_
-          (Kind.Term.parser.bind
-            Kind.PreTerm
-            Kind.Term.parser
-            λval
-            (Kind.Term.parser.bind
-              Kind.PreTerm
-              Kind.Term.parser
-              λbod
-              (Kind.Term.parser.pure
-                λscp
-                (Kind.def
-                  nam
-                  (val scp)
-                  λx (bod (Kind.Scope.extend nam x scp))
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/hol.kind2
+++ b/book/Kind/Term/parser/hol.kind2
@ -1,19 +0,0 @@
-Kind.Term.parser.hol
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "?"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "?")
-      λ_
-      (Kind.Term.parser.bind
-        String
-        Parser.name
-        λnam
-        (Kind.Term.parser.pure
-          λscp (Kind.hol nam (List.nil Kind.Term))
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/ins.kind2
+++ b/book/Kind/Term/parser/ins.kind2
@ -1,16 +0,0 @@
-Kind.Term.parser.ins
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "~"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "~")
-      λ_
-      (Kind.Term.parser.bind
-        Kind.PreTerm
-        Kind.Term.parser
-        λval (Kind.Term.parser.pure λscp (Kind.ins (val scp)))
-      )
-    )
-  )
--- a/book/Kind/Term/parser/lam.kind2
+++ b/book/Kind/Term/parser/lam.kind2
@ -1,25 +0,0 @@
-Kind.Term.parser.lam
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "λ"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "λ")
-      λ_
-      (Kind.Term.parser.bind
-        String
-        Parser.name
-        λnam
-        (Kind.Term.parser.bind
-          Kind.PreTerm
-          Kind.Term.parser
-          λbod
-          (Kind.Term.parser.pure
-            λscp
-            (Kind.lam nam λx (bod (Kind.Scope.extend nam x scp)))
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/mat.kind2
+++ b/book/Kind/Term/parser/mat.kind2
@ -1,87 +0,0 @@
-Kind.Term.parser.mat
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "switch "
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "switch ")
-      λ_
-      (Kind.Term.parser.bind
-        String
-        Parser.name
-        λnam
-        (Kind.Term.parser.bind
-          Unit
-          (Parser.text "=")
-          λ_
-          (Kind.Term.parser.bind
-            Kind.PreTerm
-            Kind.Term.parser
-            λx
-            (Kind.Term.parser.bind
-              Unit
-              (Parser.text "{")
-              λ_
-              (Kind.Term.parser.bind
-                Unit
-                (Parser.text "0")
-                λ_
-                (Kind.Term.parser.bind
-                  Unit
-                  (Parser.text ":")
-                  λ_
-                  (Kind.Term.parser.bind
-                    Kind.PreTerm
-                    Kind.Term.parser
-                    λz
-                    (Kind.Term.parser.bind
-                      Unit
-                      (Parser.text "+")
-                      λ_
-                      (Kind.Term.parser.bind
-                        Unit
-                        (Parser.text ":")
-                        λ_
-                        (Kind.Term.parser.bind
-                          Kind.PreTerm
-                          Kind.Term.parser
-                          λs
-                          (Kind.Term.parser.bind
-                            Unit
-                            (Parser.text "}")
-                            λ_
-                            (Kind.Term.parser.bind
-                              Unit
-                              (Parser.text ":")
-                              λ_
-                              (Kind.Term.parser.bind
-                                Kind.PreTerm
-                                Kind.Term.parser
-                                λp
-                                (Kind.Term.parser.pure
-                                  λscp
-                                  (Kind.mat
-                                    nam
-                                    (x scp)
-                                    (z scp)
-                                    λx
-                                    (s (Kind.Scope.extend (String.concat nam "-1") x scp))
-                                    λx (p (Kind.Scope.extend nam x scp))
-                                  )
-                                )
-                              )
-                            )
-                          )
-                        )
-                      )
-                    )
-                  )
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/num.kind2
+++ b/book/Kind/Term/parser/num.kind2
@ -1,16 +0,0 @@
-Kind.Term.parser.num
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    ""
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "")
-      λ_
-      (Kind.Term.parser.bind
-        U48
-        U48.parser.decimal
-        λnum (Kind.Term.parser.pure λscp (Kind.num num))
-      )
-    )
-  )
--- a/book/Kind/Term/parser/op2.kind2
+++ b/book/Kind/Term/parser/op2.kind2
@ -1,34 +0,0 @@
-Kind.Term.parser.op2
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "("
-    (Kind.Term.parser.bind
-      _
-      (Parser.text "(")
-      λ_
-      (Kind.Term.parser.bind
-        _
-        Kind.Oper.parser
-        λopr
-        (Kind.Term.parser.bind
-          Kind.PreTerm
-          Kind.Term.parser
-          λfst
-          (Kind.Term.parser.bind
-            _
-            Kind.Term.parser
-            λsnd
-            (Kind.Term.parser.bind
-              Unit
-              (Parser.text ")")
-              λ_
-              (Kind.Term.parser.pure
-                λscp (Kind.op2 opr (fst scp) (snd scp))
-              )
-            )
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/pure.kind2
+++ b/book/Kind/Term/parser/pure.kind2
@ -1,3 +0,0 @@
-Kind.Term.parser.pure
-: ∀(value: Kind.PreTerm) (Parser Kind.PreTerm)
-= (Parser.pure Kind.PreTerm)
--- a/book/Kind/Term/parser/set.kind2
+++ b/book/Kind/Term/parser/set.kind2
@ -1,11 +0,0 @@
-Kind.Term.parser.set
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "*"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "*")
-      λ_ (Kind.Term.parser.pure λscp Kind.set)
-    )
-  )
--- a/book/Kind/Term/parser/slf.kind2
+++ b/book/Kind/Term/parser/slf.kind2
@ -1,25 +0,0 @@
-Kind.Term.parser.slf
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "$"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "$")
-      λ_
-      (Kind.Term.parser.bind
-        String
-        Parser.name
-        λnam
-        (Kind.Term.parser.bind
-          Kind.PreTerm
-          Kind.Term.parser
-          λbod
-          (Kind.Term.parser.pure
-            λscp
-            (Kind.slf nam λx (bod (Kind.Scope.extend nam x scp)))
-          )
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/str.kind2
+++ b/book/Kind/Term/parser/str.kind2
@ -1,25 +0,0 @@
-Kind.Term.parser.str
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    String.quote
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text String.quote)
-      λ_
-      (Kind.Term.parser.bind
-        String
-        (Parser.until
-          Char
-          (Parser.test String.quote)
-          Parser.char
-        )
-        λchars
-        (Kind.Term.parser.bind
-          Unit
-          (Parser.text String.quote)
-          λ_ (Kind.Term.parser.pure λscp (Kind.txt chars))
-        )
-      )
-    )
-  )
--- a/book/Kind/Term/parser/u60.kind2
+++ b/book/Kind/Term/parser/u60.kind2
@ -1,11 +0,0 @@
-Kind.Term.parser.u60
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.text
-    Kind.PreTerm
-    "U48"
-    (Kind.Term.parser.bind
-      Unit
-      (Parser.text "U48")
-      λ_ (Kind.Term.parser.pure λscp Kind.u60)
-    )
-  )
--- a/book/Kind/Term/parser/var.kind2
+++ b/book/Kind/Term/parser/var.kind2
@ -1,11 +0,0 @@
-Kind.Term.parser.var
-: (Parser.Guard Kind.PreTerm)
-= (Parser.Guard.pass
-    Kind.PreTerm
-    (Kind.Term.parser.bind
-      String
-      Parser.name
-      λnam
-      (Kind.Term.parser.pure λscp (Kind.Scope.find nam scp))
-    )
-  )
--- a/book/Kind/Term/show.kind2
+++ b/book/Kind/Term/show.kind2
@ -1,4 +0,0 @@
-Kind.Term.show
-: ∀(term: Kind.Term) ∀(dep: Nat) String
-= λterm λdep
-  (String.Chunk.build (Kind.Term.show.go term dep))
--- a/book/Kind/Term/show/go.kind2
+++ b/book/Kind/Term/show/go.kind2
@ -1,192 +0,0 @@
-Kind.Term.show.go
-: ∀(term: Kind.Term) ∀(dep: Nat) String.Chunk
-= λterm λdep
-  use P = λX String.Chunk
-  use all = λnam λinp λbod λnil
-    (Kind.Text.show.go
-      "∀("
-      (Kind.Text.show.go
-        nam
-        (Kind.Text.show.go
-          ": "
-          (Kind.Term.show.go
-            inp
-            dep
-            (Kind.Text.show.go
-              ") "
-              (Kind.Term.show.go
-                (bod (Kind.var nam dep))
-                (Nat.succ dep)
-                nil
-              )
-            )
-          )
-        )
-      )
-    )
-  use lam = λnam λbod λnil
-    (Kind.Text.show.go
-      "λ"
-      (Kind.Text.show.go
-        nam
-        (Kind.Text.show.go
-          " "
-          (Kind.Term.show.go
-            (bod (Kind.var nam dep))
-            (Nat.succ dep)
-            nil
-          )
-        )
-      )
-    )
-  use app = λfun λarg λnil
-    (Kind.Text.show.go
-      "("
-      (Kind.Term.show.go
-        fun
-        dep
-        (Kind.Text.show.go
-          " "
-          (Kind.Term.show.go arg dep (Kind.Text.show.go ")" nil))
-        )
-      )
-    )
-  use ann = λval λtyp λnil
-    (Kind.Text.show.go
-      "{"
-      (Kind.Term.show.go
-        val
-        dep
-        (Kind.Text.show.go
-          " : "
-          (Kind.Term.show.go typ dep (Kind.Text.show.go "}" nil))
-        )
-      )
-    )
-  use slf = λnam λbod λnil
-    (Kind.Text.show.go
-      "$"
-      (Kind.Text.show.go
-        nam
-        (Kind.Text.show.go
-          " "
-          (Kind.Term.show.go
-            (bod (Kind.var nam dep))
-            (Nat.succ dep)
-            nil
-          )
-        )
-      )
-    )
-  use ins = λval λnil
-    (Kind.Text.show.go "~" (Kind.Term.show.go val dep nil))
-  use ref = λnam λval λnil (Kind.Text.show.go nam nil)
-  use def = λnam λval λbod λnil
-    (Kind.Text.show.go
-      "use "
-      (Kind.Text.show.go
-        nam
-        (Kind.Text.show.go
-          " = "
-          (Kind.Term.show.go
-            val
-            dep
-            (Kind.Text.show.go
-              "; "
-              (Kind.Term.show.go
-                (bod (Kind.var nam dep))
-                (Nat.succ dep)
-                nil
-              )
-            )
-          )
-        )
-      )
-    )
-  use set = λnil (Kind.Text.show.go "*" nil)
-  use u60 = λnil (Kind.Text.show.go "U48" nil)
-  use num = λval λnil (Kind.Text.show.go "" (U48.show.go val nil))
-  use op2 = λopr λfst λsnd λnil
-    (Kind.Text.show.go
-      "("
-      (Kind.Oper.show.go
-        opr
-        (Kind.Text.show.go
-          " "
-          (Kind.Term.show.go
-            fst
-            dep
-            (Kind.Text.show.go
-              " "
-              (Kind.Term.show.go snd dep (Kind.Text.show.go ")" nil))
-            )
-          )
-        )
-      )
-    )
-  use mat = λnam λx λz λs λp λnil
-    (Kind.Text.show.go
-      "switch "
-      (Kind.Text.show.go
-        nam
-        (Kind.Text.show.go
-          " = "
-          (Kind.Term.show.go
-            x
-            dep
-            (Kind.Text.show.go
-              " { 0: "
-              (Kind.Term.show.go
-                z
-                dep
-                (Kind.Text.show.go
-                  "; _: "
-                  (Kind.Term.show.go
-                    (s (Kind.var (String.concat nam "-1") dep))
-                    (Nat.succ dep)
-                    (Kind.Text.show.go
-                      " }: "
-                      (Kind.Term.show.go
-                        (p (Kind.var nam dep))
-                        (Nat.succ dep)
-                        nil
-                      )
-                    )
-                  )
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  use txt = λtext λnil
-    (Kind.Text.show.go
-      String.quote
-      (Kind.Text.show.go
-        text
-        (Kind.Text.show.go String.quote nil)
-      )
-    )
-  use hol = λnam λctx λnil
-    (Kind.Text.show.go "?" (Kind.Text.show.go nam nil))
-  use var = λnam λidx λnil (Kind.Text.show.go nam nil)
-  (~term
-    P
-    all
-    lam
-    app
-    ann
-    slf
-    ins
-    ref
-    def
-    set
-    u60
-    num
-    op2
-    mat
-    txt
-    hol
-    var
-  )
--- a/book/Kind/Text.kind2
+++ b/book/Kind/Text.kind2
@ -1,3 +0,0 @@
-Kind.Text
-: *
-= String
--- a/book/Kind/Text/show/go.kind2
+++ b/book/Kind/Text/show/go.kind2
@ -1,3 +0,0 @@
-Kind.Text.show.go
-: ∀(text: Kind.Text) String.Chunk
-= String.Chunk.from_string
--- a/book/Kind/_.kind2
+++ b/book/Kind/_.kind2
@ -1,33 +0,0 @@
-Kind
-: String
-= use a = (Kind.lam
-      "f"
-      λf (Kind.lam "x" λx (Kind.app f (Kind.app f x)))
-    )
-  use b = (Kind.lam
-      "f"
-      λf (Kind.lam "x" λx (Kind.app f (Kind.app f x)))
-    )
-  use Test = (Kind.all
-      "A"
-      Kind.set
-      λA
-      (Kind.all
-        "B"
-        Kind.set
-        λB (Kind.all "a" A λa (Kind.all "b" B λb B))
-      )
-    )
-  use test = (Kind.lam
-      "A"
-      λA
-      (Kind.lam
-        "B"
-        λB (Kind.lam "a" λa (Kind.lam "b" λb b))
-      )
-    )
-  use P = λx String
-  use some = λvalue (Kind.Term.show value Nat.zero)
-  use none = "error"
-  use chk = (Kind.check test Test Nat.zero)
-  (~chk P some none)
--- a/book/Kind/all.kind2
+++ b/book/Kind/all.kind2
@ -1,8 +0,0 @@
-Kind.all
-: ∀(nam: String)
-  ∀(inp: Kind.Term)
-  ∀(bod: ∀(x: Kind.Term) Kind.Term)
-  Kind.Term
-= λnam λinp λbod
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (all nam inp bod)
--- a/book/Kind/ann.kind2
+++ b/book/Kind/ann.kind2
@ -1,5 +0,0 @@
-Kind.ann
-: ∀(val: Kind.Term) ∀(typ: Kind.Term) Kind.Term
-= λval λtyp
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (ann val typ)
--- a/book/Kind/app.kind2
+++ b/book/Kind/app.kind2
@ -1,5 +0,0 @@
-Kind.app
-: ∀(fun: Kind.Term) ∀(arg: Kind.Term) Kind.Term
-= λfun λarg
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (app fun arg)
--- a/book/Kind/check.kind2
+++ b/book/Kind/check.kind2
@ -1,90 +0,0 @@
-Kind.check
-: ∀(term: Kind.Term) ∀(type: Kind.Term) ∀(dep: Nat)
-  (Maybe Kind.Term)
-= λterm λtype λdep
-  use bind = (Maybe.bind Kind.Term Kind.Term)
-  use pure = (Maybe.some Kind.Term)
-  use none = (Maybe.none Kind.Term)
-  use P = λx ∀(type: Kind.Term) ∀(dep: Nat) (Maybe Kind.Term)
-  use all = λterm.nam λterm.inp λterm.bod λtype λdep
-    (Kind.verify
-      (Kind.all term.nam term.inp term.bod)
-      type
-      dep
-    )
-  use lam = λterm.nam λterm.bod λtype λdep
-    (Kind.if.all
-      (Kind.reduce Bool.true type)
-      ∀(dep: Nat) ∀(term.bod: ∀(x: Kind.Term) Kind.Term)
-      (Maybe Kind.Term)
-      λtype.nam λtype.inp λtype.bod λdep λterm.bod
-      use ann = (Kind.ann (Kind.var term.nam dep) type.inp)
-      use term = (term.bod ann)
-      use type = (type.bod ann)
-      (Kind.check term type (Nat.succ dep))
-      λtype λdep λterm.bod
-      (Kind.infer (Kind.lam term.nam term.bod) dep)
-      dep
-      term.bod
-    )
-  use app = λterm.fun λterm.arg λtype λdep
-    (Kind.verify (Kind.app term.fun term.arg) type dep)
-  use ann = λval λtyp λtype λdep
-    (Kind.verify (Kind.ann val typ) type dep)
-  use slf = λterm.nam λterm.bod λtype λdep
-    (Kind.verify (Kind.slf term.nam term.bod) type dep)
-  use ins = λterm.val λtype λdep
-    (Kind.if.slf
-      (Kind.reduce Bool.true type)
-      ∀(term.val: Kind.Term) (Maybe Kind.Term)
-      λtype.nam λtype.bod λterm.val
-      (Kind.check term.val (type.bod (Kind.ins term.val)) dep)
-      λtype λterm.val (Kind.infer (Kind.ins term.val) dep)
-      term.val
-    )
-  use ref = λterm.nam λterm.val λtype λdep
-    (Kind.check term.val type dep)
-  use def = λterm.nam λterm.val λterm.bod λtype λdep
-    (Kind.check (term.bod term.val) type (Nat.succ dep))
-  use set = λtype λdep (Kind.verify Kind.set type dep)
-  use u60 = λtype λdep (Kind.verify Kind.u60 type dep)
-  use num = λterm.num λtype λdep
-    (Kind.verify (Kind.num term.num) type dep)
-  use op2 = λterm.opr λterm.fst λterm.snd λtype λdep
-    (Kind.verify
-      (Kind.op2 term.opr term.fst term.snd)
-      type
-      dep
-    )
-  use mat = λterm.nam λterm.x λterm.z λterm.s λterm.p λtype λdep
-    (Kind.verify
-      (Kind.mat term.nam term.x term.z term.s term.p)
-      type
-      dep
-    )
-  use txt = λterm.txt λtype λdep
-    (Kind.verify (Kind.txt term.txt) type dep)
-  use hol = λterm.nam λterm.ctx λtype λdep (pure Kind.set)
-  use var = λterm.nam λterm.idx λtype λdep
-    (Kind.verify (Kind.var term.nam term.idx) type dep)
-  (~term
-    P
-    all
-    lam
-    app
-    ann
-    slf
-    ins
-    ref
-    def
-    set
-    u60
-    num
-    op2
-    mat
-    txt
-    hol
-    var
-    type
-    dep
-  )
--- a/book/Kind/comparer.kind2
+++ b/book/Kind/comparer.kind2
@ -1,145 +0,0 @@
-Kind.comparer
-: ∀(rec: 
-    ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool
-  )
-  ∀(a: Kind.Term)
-  ∀(b: Kind.Term)
-  ∀(dep: Nat)
-  Bool
-= λrec λa λb λdep
-  use VAR = Kind.var
-  use SUC = Nat.succ
-  use a = (Kind.skip a)
-  use b = (Kind.skip b)
-  use R = ∀(b: Kind.Term) ∀(dep: Nat) Bool
-  use Y = λa.nam λa.ctx λb λdep Bool.true
-  use N = λa λb λdep
-    use R = ∀(dep: Nat) ∀(a: Kind.Term) Bool
-    use Y = λb.nam λb.ctx λdep λa Bool.true
-    use N = λb λdep λa
-      use P = λx ∀(b: Kind.Term) ∀(dep: Nat) Bool
-      use all = λa.nam λa.inp λa.bod λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.nam λb.inp λb.bod λdep
-          (Bool.and
-            (rec a.inp b.inp dep)
-            (rec
-              (a.bod (VAR a.nam dep))
-              (b.bod (VAR b.nam dep))
-              (SUC dep)
-            )
-          )
-        use N = λval λdep Bool.false
-        (Kind.if.all b P Y N dep)
-      use lam = λa.nam λa.bod λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.nam λb.bod λdep
-          (rec
-            (a.bod (VAR a.nam dep))
-            (b.bod (VAR b.nam dep))
-            (SUC dep)
-          )
-        use N = λval λdep Bool.false
-        (Kind.if.lam b P Y N dep)
-      use app = λa.fun λa.arg λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.fun λb.arg λdep
-          (Bool.and (rec a.fun b.fun dep) (rec a.arg b.arg dep))
-        use N = λval λdep Bool.false
-        (Kind.if.app b P Y N dep)
-      use ann = λa.val λa.typ λb λdep Bool.false
-      use slf = λa.nam λa.bod λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.nam λb.bod λdep
-          (rec
-            (a.bod (VAR a.nam dep))
-            (b.bod (VAR b.nam dep))
-            (SUC dep)
-          )
-        use N = λval λdep Bool.false
-        (Kind.if.slf b P Y N dep)
-      use ins = λa.val λb λdep Bool.false
-      use ref = λa.nam λa.val λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.nam λb.val λdep (String.equal a.nam b.nam)
-        use N = λval λdep Bool.false
-        (Kind.if.ref b P Y N dep)
-      use def = λa.nam λa.val λa.bod λb λdep Bool.false
-      use set = λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λdep Bool.true
-        use F = λval λdep Bool.false
-        (Kind.if.set b P Y F dep)
-      use u60 = λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λdep Bool.true
-        use N = λval λdep Bool.false
-        (Kind.if.u60 b P Y N dep)
-      use num = λa.val λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.val λdep (U48.equal a.val b.val)
-        use N = λval λdep Bool.false
-        (Kind.if.num b P Y N dep)
-      use op2 = λa.opr λa.fst λa.snd λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.opr λb.fst λb.snd λdep
-          (Bool.and (rec a.fst b.fst dep) (rec a.snd b.snd dep))
-        use N = λval λdep Bool.false
-        (Kind.if.op2 b P Y N dep)
-      use mat = λa.nam λa.x λa.z λa.s λa.p λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.nam λb.x λb.z λb.s λb.p λdep
-          (Bool.and
-            (rec a.x b.x dep)
-            (Bool.and
-              (rec a.z b.z dep)
-              (Bool.and
-                (rec
-                  (a.s (VAR (String.concat a.nam "-1") dep))
-                  (b.s (VAR (String.concat b.nam "-1") dep))
-                  (SUC dep)
-                )
-                (rec
-                  (a.p (VAR a.nam dep))
-                  (b.p (VAR b.nam dep))
-                  (SUC dep)
-                )
-              )
-            )
-          )
-        use N = λval λdep Bool.false
-        (Kind.if.mat b P Y N dep)
-      use txt = λa.txt λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.txt λdep (String.equal a.txt b.txt)
-        use N = λval λdep Bool.false
-        (Kind.if.txt b P Y N dep)
-      use hol = λa.nam λa.ctx λb λdep Bool.false
-      use var = λa.nam λa.idx λb λdep
-        use P = ∀(dep: Nat) Bool
-        use Y = λb.nam λb.idx λdep (Nat.equal a.idx b.idx)
-        use N = λval λdep Bool.false
-        (Kind.if.var b P Y N dep)
-      (~a
-        P
-        all
-        lam
-        app
-        ann
-        slf
-        ins
-        ref
-        def
-        set
-        u60
-        num
-        op2
-        mat
-        txt
-        hol
-        var
-        b
-        dep
-      )
-    (Kind.if.hol b R Y N dep a)
-  (Kind.if.hol a R Y N b dep)
--- a/book/Kind/def.kind2
+++ b/book/Kind/def.kind2
@ -1,8 +0,0 @@
-Kind.def
-: ∀(nam: String)
-  ∀(val: Kind.Term)
-  ∀(bod: ∀(x: Kind.Term) Kind.Term)
-  Kind.Term
-= λnam λval λbod
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (def nam val bod)
--- a/book/Kind/equal.kind2
+++ b/book/Kind/equal.kind2
@ -1,4 +0,0 @@
-Kind.equal
-: ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool
-= λa λb λdep
-  (Kind.equal.minor (Kind.identical a b dep) a b dep)
--- a/book/Kind/equal/enter.kind2
+++ b/book/Kind/equal/enter.kind2
@ -1,11 +0,0 @@
-Kind.equal.enter
-: ∀(e: Bool)
-  ∀(a: Kind.Term)
-  ∀(b: Kind.Term)
-  ∀(dep: Nat)
-  Bool
-= λe λa λb λdep
-  use P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool
-  use true = λa λb λdep Bool.true
-  use false = λa λb λdep (Kind.comparer Kind.equal a b dep)
-  (~e P true false a b dep)
--- a/book/Kind/equal/major.kind2
+++ b/book/Kind/equal/major.kind2
@ -1,19 +0,0 @@
-Kind.equal.major
-: ∀(e: Bool)
-  ∀(a: Kind.Term)
-  ∀(b: Kind.Term)
-  ∀(dep: Nat)
-  Bool
-= λe λa λb λdep
-  use P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool
-  use true = λa λb λdep Bool.true
-  use false = λa λb λdep
-    use a_wnf = (Kind.reduce Bool.true a)
-    use b_wnf = (Kind.reduce Bool.true b)
-    (Kind.equal.enter
-      (Kind.identical a_wnf b_wnf dep)
-      a_wnf
-      b_wnf
-      dep
-    )
-  (~e P true false a b dep)
--- a/book/Kind/equal/minor.kind2
+++ b/book/Kind/equal/minor.kind2
@ -1,19 +0,0 @@
-Kind.equal.minor
-: ∀(e: Bool)
-  ∀(a: Kind.Term)
-  ∀(b: Kind.Term)
-  ∀(dep: Nat)
-  Bool
-= λe λa λb λdep
-  use P = λx ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool
-  use true = λa λb λdep Bool.true
-  use false = λa λb λdep
-    use a_wnf = (Kind.reduce Bool.false a)
-    use b_wnf = (Kind.reduce Bool.false b)
-    (Kind.equal.major
-      (Kind.identical a_wnf b_wnf dep)
-      a_wnf
-      b_wnf
-      dep
-    )
-  (~e P true false a b dep)
--- a/book/Kind/export.kind2
+++ b/book/Kind/export.kind2
@ -1,6 +0,0 @@
-Kind.export
-: Unit
-= use x = Kind.Book.get_refs
-  use x = Kind.Book.parse
-  use x = Kind.Book.to_hvm
-  Unit.one
--- a/book/Kind/hol.kind2
+++ b/book/Kind/hol.kind2
@ -1,5 +0,0 @@
-Kind.hol
-: ∀(nam: String) ∀(ctx: (List Kind.Term)) Kind.Term
-= λnam λctx
-  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
-  (hol nam ctx)
--- a/book/Kind/identical.kind2
+++ b/book/Kind/identical.kind2
@ -1,3 +0,0 @@
-Kind.identical
-: ∀(a: Kind.Term) ∀(b: Kind.Term) ∀(dep: Nat) Bool
-= λa λb λdep (Kind.comparer Kind.identical a b dep)
--- a/book/Kind/if/all.kind2
+++ b/book/Kind/if/all.kind2
@ -1,58 +0,0 @@
-Kind.if.all
-: ∀(term: Kind.Term)
-  ∀(P: *)
-  ∀(Y: 
-    ∀(nam: String)
-    ∀(inp: Kind.Term)
-    ∀(bod: ∀(x: Kind.Term) Kind.Term)
-    P
-  )
-  ∀(N: ∀(val: Kind.Term) P)
-  P
-= λterm λP λY λN
-  use P = λx
-    ∀(Y: 
-      ∀(nam: String)
-      ∀(inp: Kind.Term)
-      ∀(bod: ∀(x: Kind.Term) Kind.Term)
-      P
-    )
-    ∀(N: ∀(val: Kind.Term) P)
-    P
-  use all = λnam λinp λbod λY λN (Y nam inp bod)
-  use lam = λnam λbod λY λN (N (Kind.lam nam bod))
-  use app = λfun λarg λY λN (N (Kind.app fun arg))
-  use ann = λval λtyp λY λN (N (Kind.ann val typ))
-  use slf = λnam λbod λY λN (N (Kind.slf nam bod))
-  use ins = λval λY λN (N (Kind.ins val))
-  use ref = λnam λval λY λN (N (Kind.ref nam val))
-  use def = λnam λval λbod λY λN (N (Kind.def nam val bod))
-  use set = λY λN (N Kind.set)
-  use u60 = λY λN (N Kind.u60)
-  use num = λval λY λN (N (Kind.num val))
-  use op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd))
-  use mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p))
-  use txt = λlit λY λN (N (Kind.txt lit))
-  use hol = λnam λctx λY λN (N (Kind.hol nam ctx))
-  use var = λnam λidx λY λN (N (Kind.var nam idx))
-  (~term
-    P
-    all
-    lam
-    app
-    ann
-    slf
-    ins
-    ref
-    def
-    set
-    u60
-    num
-    op2
-    mat
-    txt
-    hol
-    var
-    Y
-    N
-  )
--- a/book/Kind/if/ann.kind2
+++ b/book/Kind/if/ann.kind2
@ -1,48 +0,0 @@
-Kind.if.ann
-: ∀(term: Kind.Term)
-  ∀(P: *)
-  ∀(Y: ∀(val: Kind.Term) ∀(typ: Kind.Term) P)
-  ∀(N: ∀(val: Kind.Term) P)
-  P
-= λterm λP λY λN
-  use P = λx
-    ∀(Y: ∀(val: Kind.Term) ∀(typ: Kind.Term) P)
-    ∀(N: ∀(val: Kind.Term) P)
-    P
-  use all = λnam λinp λbod λY λN (N (Kind.all nam inp bod))
-  use lam = λnam λbod λY λN (N (Kind.lam nam bod))
-  use app = λfun λarg λY λN (N (Kind.app fun arg))
-  use ann = λval λtyp λY λN (Y val typ)
-  use slf = λnam λbod λY λN (N (Kind.slf nam bod))
-  use ins = λval λY λN (N (Kind.ins val))
-  use ref = λnam λval λY λN (N (Kind.ref nam val))
-  use def = λnam λval λbod λY λN (N (Kind.def nam val bod))
-  use set = λY λN (N Kind.set)
-  use u60 = λY λN (N Kind.u60)
-  use num = λval λY λN (N (Kind.num val))
-  use op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd))
-  use mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p))
-  use txt = λlit λY λN (N (Kind.txt lit))
-  use hol = λnam λctx λY λN (N (Kind.hol nam ctx))
-  use var = λnam λidx λY λN (N (Kind.var nam idx))
-  (~term
-    P
-    all
-    lam
-    app
-    ann
-    slf
-    ins
-    ref
-    def
-    set
-    u60
-    num
-    op2
-    mat
-    txt
-    hol
-    var
-    Y
-    N
-  )
--- a/book/Kind/if/app.kind2
+++ b/book/Kind/if/app.kind2
@ -1,48 +0,0 @@
-Kind.if.app
-: ∀(term: Kind.Term)
-  ∀(P: *)
-  ∀(Y: ∀(fun: Kind.Term) ∀(arg: Kind.Term) P)
-  ∀(N: ∀(val: Kind.Term) P)
-  P
-= λterm λP λY λN
-  use P = λx
-    ∀(Y: ∀(fun: Kind.Term) ∀(arg: Kind.Term) P)
-    ∀(N: ∀(val: Kind.Term) P)
-    P
-  use all = λnam λinp λbod λY λN (N (Kind.all nam inp bod))
-  use lam = λnam λbod λY λN (N (Kind.lam nam bod))
-  use app = λfun λarg λY λN (Y fun arg)
-  use ann = λval λtyp λY λN (N (Kind.ann val typ))
-  use slf = λnam λbod λY λN (N (Kind.slf nam bod))
-  use ins = λval λY λN (N (Kind.ins val))
-  use ref = λnam λval λY λN (N (Kind.ref nam val))
-  use def = λnam λval λbod λY λN (N (Kind.def nam val bod))
-  use set = λY λN (N Kind.set)
-  use u60 = λY λN (N Kind.u60)
-  use num = λval λY λN (N (Kind.num val))
-  use op2 = λopr λfst λsnd λY λN (N (Kind.op2 opr fst snd))
-  use mat = λnam λx λz λs λp λY λN (N (Kind.mat nam x z s p))
-  use txt = λlit λY λN (N (Kind.txt lit))
-  use hol = λnam λctx λY λN (N (Kind.hol nam ctx))
-  use var = λnam λidx λY λN (N (Kind.var nam idx))
-  (~term
-    P
-    all
-    lam
-    app
-    ann
-    slf
-    ins
-    ref
-    def
-    set
-    u60
-    num
-    op2
-    mat
-    txt
-    hol
-    var
-    Y
-    N
-  )
--- a/Show More
+++ b/Show More