Merge branch 'uwu-tech:master' into master

base/App/HotS.kind

@@ -9,7 +9,16 @@ App.HotS.State: App.State
 // Initial state
 App.HotS.init: App.Init<App.HotS.State>
   let bids = {} :: Map<App.HotS.Bid>
-  let cash = {} :: Map<Nat>
+  let cash = {
+    "Green": 23
+    "Blue": 24
+    "Red": 25
+    "Yellow": 26
+    "Purple": 27
+    "White": 28
+    "Black": 29
+    "Orange": 30
+  } :: Map<Nat>
   App.Store.new<App.HotS.State>(App.HotS.State.Local.new(false, "", ""), App.HotS.State.Global.new(bids, cash))
 
 type App.HotS.State.Local {
@@ -229,8 +238,9 @@ App.HotS.post: App.Post<App.HotS.State>
       let team_size = List.count!((x) String.eql(x@team,post.team), Map.values!(global.bids))
       let rebuy = (case global.bids{post.player} as bid { none: false, some: String.eql(bid.value@team,post.team) })
       let can_buy = if rebuy then team_cash >=? 1 else (team_cash >=? player_value) && (team_size <? 6)
+      let player_exists = Map.has!(post.player, App.HotS.players)
       //log(Nat.show(team_cash) | " >=? " | Nat.show(player_value))
-      if can_buy then
+      if can_buy && player_exists then
         log(post.team | " purchased " | post.player)
         let bids = global.bids{post.player} <- App.HotS.Bid.new(player_value + 1, post.team)
         let cash = global.cash

base/Ether/RLP/encode.kind

@@ -12,7 +12,7 @@ Ether.RLP.encode.bytes(tree : Ether.RLP.Tree) : List<Bits>
         for item in tree.value with bytes :
           bytes ++ Ether.RLP.encode.bytes(item)
         let bytes_size = List.foldr!!(0, (x, y) Ether.Bits.get_bytes_size(x) + y, bytes)    
-        log("first encoding " | Nat.show(bytes_size))
+    //    log("first encoding " | Nat.show(bytes_size))
         Ether.RPL.encode_length(bytes_size, 192) ++ bytes
   }
 //56 + 
@@ -23,7 +23,7 @@ Ether.RPL.encode_length(value : Nat, offSet : Nat) : List<Bits>
     18446744073709551616 : 
       let binary_encoding = Ether.RPL.encode.binary(value)
       let len = List.foldr!!(0, (x, y) Ether.Bits.get_bytes_size(x) + y, binary_encoding)
-      log(Nat.show(value) | " " | Bits.show(List.foldr!!(Bits.e, Bits.concat, [Nat.to_bits(len + offSet + 55)] ++ binary_encoding)))
+  //    log(Nat.show(value) | " " | Bits.show(List.foldr!!(Bits.e, Bits.concat, [Nat.to_bits(len + offSet + 55)] ++ binary_encoding)))
 
       [Nat.to_bits(len + offSet + 55)] ++ binary_encoding
   } default [] // This case has to be treated within a proof

base/Ether/RLP/proof/encode.kind

@@ -1,9 +1,166 @@
-Bits.concat.go(a: Bits, b: Bits): Bits
-  case a {
-    e: b,
-    o: Bits.concat(a.pred, Bits.o(b))
-    i: Bits.concat(a.pred, Bits.i(b))
-  }
+
+
+Ether.RLP.proof.pad_bytes(bits : Bits) : Bits
+  let size = Bits.length(bits)
+  Bits.trim(((8 * ((size + 7) / 8)) - size) + size, bits)
+  
+
+Bits.size.rec(x : Bits, n : Nat) : 
+  Nat.succ(Bits.length.go(x, n)) == Bits.length.go(x, Nat.succ(n))
+    case x {
+      e : refl
+      i : Bits.size.rec(x.pred, Nat.succ(n))
+      o : Bits.size.rec(x.pred, Nat.succ(n))
+    }!
+
+Ether.RLP.proof.add_self_absurd(x : Nat, n: Nat) : Equal(Nat, Nat.add(n, Nat.succ(x)), n) -> Empty
+  case n {
+    succ : 
+      (H)
+         let H = Nat.succ_inj!!(H)
+         let qed = Ether.RLP.proof.add_self_absurd(x, n.pred, H)
+         qed
+    zero : (H) Nat.succ_neq_zero!(H)
+  }!
+  
+Ether.RLP.proof.add_injective(x : Nat, y : Nat, n : Nat, H : Nat.add(Nat.succ(n), x) == Nat.add(Nat.succ(n), y)) : x == y
+  case x with H {
+    succ : case y with H {
+      succ : 
+        let com_H = Nat.add.comm(Nat.succ(n), Nat.succ(x.pred))
+        let com_H2 = Nat.add.comm(Nat.succ(n), Nat.succ(y.pred))
+        let H_rewrite = H :: rewrite Y in Y == _ with com_H
+        let H_rewrite = H_rewrite :: rewrite Y in _ == Y with com_H2
+        let H_rewrite_inj = Nat.succ_inj!!(H_rewrite)
+        let H_rewrite_inj = H_rewrite_inj :: rewrite Y in Y == _ with Nat.add.comm(x.pred, Nat.succ(n))
+        let H_rewrite_inj = H_rewrite_inj :: rewrite Y in _ == Y with Nat.add.comm(y.pred, Nat.succ(n))
+        let H2 = Ether.RLP.proof.add_injective(x.pred, y.pred, n, H_rewrite_inj)
+        Equal.apply!!!!(Nat.succ, H2)
+      zero : 
+        let rewrite_0_com = 
+          Nat.add.comm(Nat.succ(n), 0)
+        let H = H :: rewrite Y in _ == Y with rewrite_0_com
+        let absurd = Ether.RLP.proof.add_self_absurd!!(H)
+        Empty.absurd!(absurd)
+    }!
+    zero : case y with H {
+      succ : 
+        let H = mirror(H)
+        let rewrite_0_com = Nat.add.comm(Nat.succ(n), 0)
+        let H = H :: rewrite Y in _ == Y with rewrite_0_com
+        let absurd = Ether.RLP.proof.add_self_absurd!!(H)
+        Empty.absurd!(absurd)
+      zero : refl
+    }!
+  }!
+
+Ether.RLP.proof.mul_injective(x : Nat, y : Nat, n : Nat, H : Nat.mul(Nat.succ(n), x) == Nat.mul(Nat.succ(n), y)) : x == y
+  case x with H {
+    succ : case y with H {
+      succ : 
+        let inj_add = Ether.RLP.proof.add_injective(Nat.mul(Nat.succ(n), x.pred), Nat.mul(Nat.succ(n), y.pred), n, H)
+        let H = Ether.RLP.proof.mul_injective(x.pred, y.pred, n, inj_add)
+        Equal.apply!!!!(Nat.succ, H)
+      zero : 
+        let H4 = Nat.succ_neq_zero!(H)
+        Empty.absurd!(H4)
+     }!
+    zero : case y with H {
+      succ : 
+       let H2 = refl :: 0 == Nat.mul(Nat.succ(n),0)
+       let H4 = Nat.succ_neq_zero!(mirror(H))
+       Empty.absurd!(H4)
+      zero : 
+        refl
+    }!
+  }!
+
+Ether.RLP.proof.succ_pad_nat(x : Bits) : 
+  Bits.to_nat(Bits.trim(Bits.length(x), x)) == Bits.to_nat(x)
+  case x {
+    e : refl 
+    o : 
+      let remove_tail_rec = Bits.size.rec(x.pred, 0)
+      let refl_cont =
+        refl :: 
+          Bits.length.go(x.pred, 1) == Bits.length(Bits.o(x.pred))
+      case refl_cont {
+        refl : 
+          case remove_tail_rec {
+            refl : 
+              let rec = Ether.RLP.proof.succ_pad_nat(x.pred)
+              let rec = Equal.apply!!!!(Nat.mul(2), rec)
+              rec
+          }!
+        }!
+    i : 
+      let remove_tail_rec = Bits.size.rec(x.pred, 0)
+      let refl_cont =
+        refl :: 
+          Bits.length.go(x.pred, 1) == Bits.length(Bits.i(x.pred))
+      case refl_cont {
+        refl : 
+          case remove_tail_rec {
+            refl : 
+              let rec = Ether.RLP.proof.succ_pad_nat(x.pred)
+              let rec = Equal.apply!!!!(Nat.mul(2), rec)
+              Equal.apply(Nat, Nat, Nat.mul(2,Bits.to_nat(Bits.trim(Bits.length.go(x.pred,0),x.pred))),
+                Nat.mul(2,Bits.to_nat(x.pred)), Nat.succ, rec)
+          }!
+        }!
+  }!
+
+Ether.RLP.proof.nat_succ_pad_nat(y : Nat, x : Bits, H : 
+  Bits.to_nat(Bits.trim(y, x)) == Bits.to_nat(x)) : 
+    Bits.to_nat(Bits.trim(Nat.succ(y), x)) == Bits.to_nat(x)
+    case y with H {
+      zero : 
+        case x with H {
+          i :
+            let H = H :: 0 == Nat.succ(Nat.mul(2, Bits.to_nat(x.pred)))
+            let absurd = Nat.succ_neq_zero!(mirror(H))
+            Empty.absurd!(absurd)
+          o : 
+            let H = H :: 0 == Nat.mul(2, Bits.to_nat(x.pred))
+            H
+          e : refl
+        }!
+      succ : case x with H {
+        i : 
+          let H = H :: Nat.succ(Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,x.pred)))) == Nat.succ(Nat.mul(2, Bits.to_nat(x.pred)))
+          let H = Nat.succ_inj(Nat.mul(2,Bits.to_nat(Bits.trim(y.pred,x.pred))), Nat.mul(2,Bits.to_nat(x.pred)), H)
+          let H = Ether.RLP.proof.mul_injective(Bits.to_nat(Bits.trim(y.pred,x.pred)), Bits.to_nat(x.pred), 1, H)
+          let H2 = Ether.RLP.proof.nat_succ_pad_nat(y.pred, x.pred, H)
+          let qed = Equal.apply!!!!(Nat.succ . Nat.mul(2), H2)
+          qed
+        o :  
+          let H = H :: Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,x.pred))) == Nat.mul(2, Bits.to_nat(x.pred))
+          let H = Ether.RLP.proof.mul_injective(Bits.to_nat(Bits.trim(y.pred,x.pred)), Bits.to_nat(x.pred), 1, H)
+          let H2 = Ether.RLP.proof.nat_succ_pad_nat(y.pred, x.pred, H)
+          let qed = Equal.apply!!!!(Nat.mul(2), H2)
+          qed
+        e : 
+          let H = H :: Nat.mul(2, Bits.to_nat(Bits.trim(y.pred,Bits.e))) == Nat.mul(2, 0)
+          let absurd_mul_injective = Ether.RLP.proof.mul_injective(Bits.to_nat(Bits.trim(y.pred,Bits.e)), 0, 1, H)
+          let H2 = Ether.RLP.proof.nat_succ_pad_nat(y.pred, Bits.e, absurd_mul_injective)
+          let qed = Equal.apply!!!!(Nat.mul(2), H2)
+          qed
+      }!
+    }!
+
+Ether.RLP.proof.pad_nat(x : Bits, y : Nat) : 
+  Bits.to_nat(Bits.trim(Nat.add(y, Bits.length(x)), x)) == Bits.to_nat(x)
+  case y {
+    succ : 
+      let H = Ether.RLP.proof.pad_nat(x, y.pred)
+      Ether.RLP.proof.nat_succ_pad_nat!!(H)
+    zero : Ether.RLP.proof.succ_pad_nat(x)
+  }!
+
+Ether.RLP.proof.pad_bytes_identity(bits : Bits) : 
+  Bits.to_nat(Ether.RLP.proof.pad_bytes(bits)) == Bits.to_nat(bits)
+  Ether.RLP.proof.pad_nat(bits, Nat.sub(Nat.mul(8,Nat.div(Nat.add(Bits.length(bits),7),8)), 
+    Bits.length(bits)))
 
 Ether.RLP.proof.encode.bytes(tree : Ether.RLP.Tree) : Bits
   case tree {
@@ -19,7 +176,6 @@ Ether.RLP.proof.encode.bytes(tree : Ether.RLP.Tree) : Bits
          for item in tree.value with bytes :
            Bits.concat(bytes, Ether.RLP.proof.encode.bytes(item))
          let bytes_size = Ether.Bits.get_bytes_size(bytes)
-         log("Second encoding " | Nat.show(bytes_size))
          Bits.concat.go(Ether.RPL.proof.encode_length(bytes_size, 192), bytes)
   }
 
@@ -30,7 +186,8 @@ Ether.RPL.proof.encode_length(value : Nat, offSet : Nat) : Bits
   } default
     let binary_encoding = Ether.RPL.proof.encode.binary(value)
     let len = Ether.Bits.get_bytes_size(binary_encoding)
-    log(Nat.show(value) | " " | Bits.show(Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)))
+
+    //log(Bits.show(Nat.to_bits(len + offSet + 55)) | " " | Bits.show(Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)))
     Bits.concat.go(Nat.to_bits(len + offSet + 55), binary_encoding)
 
 Ether.RPL.proof.encode.binary(value : Nat) : Bits
@@ -45,13 +202,15 @@ Bits.break(len : Nat, bits : Bits) : Pair<Bits, Bits>
 Ether.RLP.proof.encode.read.binary(value : Bits) : Nat
   let {head, rest} = Bits.break(8, value)
   let decode = Bits.to_nat(head)
-  if (Bits.eql(rest, Bits.o(Bits.e))) then
+  if (Bits.eql(rest, Bits.e)) then
     decode
   else
     Ether.RLP.proof.encode.read.binary(rest) + (decode * 256)
 
 Ether.RLP.proof.encode.read(bits : Bits) : String
   let {byte_prefix, rest} = Bits.break(8, bits)
+  log(Bits.show(byte_prefix))
+
   "0x" | switch (Bits.ltn(byte_prefix)) {
     Ether.RLP.Constants.bits_128 : 
       String.reverse(Bits.hex.encode(bits))  // between (0, 127)
@@ -63,7 +222,10 @@ Ether.RLP.proof.encode.read(bits : Bits) : String
      let content_length = (Bits.to_nat(byte_prefix) - 183) * 8
      let {head, rest} = Bits.break(content_length, rest)
      let length = Ether.RLP.proof.encode.read.binary(head)
+     log("teste :  " | Bits.show(head))
+
      let {prefix, rest} = Bits.break(length*8, rest)
+
      String.reverse(Bits.hex.encode(byte_prefix)) | String.reverse(Bits.hex.encode(head))
        | String.reverse(Bits.hex.encode(prefix))
 

base/Ether/tests.kind

@@ -1,23 +1,14 @@
-Bits.concat.go(a: Bits, b: Bits): Bits
-  case a {
-    e: b,
-    o: Bits.concat(a.pred, Bits.o(b))
-    i: Bits.concat(a.pred, Bits.i(b))
-  }
-
 Ether.tests : _
   //let v = Ether.RLP.Tree.list(
    // [
   //    Ether.RLP.Tree.tip(Bits.read(String.reverse("1000111011111010110"))),
    //   Ether.RLP.Tree.tip(Bits.read(String.reverse("1000111011111010110")))    
 //    ])
-  let v = Ether.RLP.Tree.tip(Bits.read("1000000100000000000000000110110000000000000000000010000000000000000011011000111111111111111111111111111111111011111000000000000100011111111111111111111111111111111101111100000000000000000000000000000001000000000000000001101100100011111111111111111111111111111111101111100000000000010001111111111111111111111111111111110111110000000000000000000000000000000100000000000000000110110000000000000000000010000000000000000011011000000000000000000010110110"))
-  let test1 = Ether.RLP.proof.encode.bytes(v)
-  let test2 = Ether.RLP.encode.bytes(v)
-  log(Ether.RLP.proof.encode.read(test1))
-  log(Ether.RLP.encode.read(test2))
-  let test2 = List.foldr!!(Bits.e, Bits.concat.go, test2)
-  {test1, test2}
+  log(Nat.show(Bits.to_nat(Ether.RLP.proof.pad_bytes2(Bits.read("1010100000000000")))))
+
+  Ether.RLP.proof.pad_bytes2(Bits.read("000000001"))
+
+
   //let buffer = Buffer8.from_hex("d69429d7d1dd5b6f9c864d9db560d72a247c178ae86b0a")
   //let hash = Crypto.Keccak.hash.bytes(buffer)
   //Buffer8.to_hex(hash)  

base/Nat/AlgExp.kind

@@ -0,0 +1,48 @@
+Variadic.Equal<A: Type, B: Type>(
+  n: Nat
+  l: Variadic(n)<A, B>
+  r: Variadic(n)<A, B>
+): Variadic(n)<A, Type>
+  case n with l r {
+    zero:
+      Equal<B>(l, r)
+    succ:
+      (x) Variadic.Equal<A, B>(n.pred, l(x), r(x))
+  }!
+
+Nat.AlgExp.from_nat(n: Nat): Nat.AlgExp
+  Nat.AlgExp.const(n)
+
+Nat.AlgExp.dimension(exp: Nat.AlgExp): Nat
+  ?dimension
+
+Nat.AlgExp.substitution(exp: Nat.AlgExp): Variadic(Nat.AlgExp.dimension(exp), Nat, Nat)
+  ?substitution
+
+Nat.AlgExp.eql(exp0: Nat.AlgExp, exp1: Nat.AlgExp): Bool
+  ?equal
+
+type Nat.AlgExp {
+  const(value: Nat)
+  var(idx: Nat)
+  add(left: Nat.AlgExp, right: Nat.AlgExp)
+  mul(left: Nat.AlgExp, right: Nat.AlgExp)
+}
+
+Nat.AlgExp.decide(
+  exp0: Nat.AlgExp
+  exp1: Nat.AlgExp
+):  let eql = Nat.AlgExp.eql(exp0, exp1)
+    if eql then
+      Variadic.Equal(n, Nat.AlgExp.substitution(exp0), Nat.AlgExp.substitution(exp1))
+    else
+      Variadic.NotEqual(n, Nat.AlgExp.substitution(exp0), Nat.AlgExp.substitution(exp1))
+  ?equivalence
+
+Test(a: Nat, b: Nat): Equal<Nat>((a + b) * (a + b), (a * a) + (2 * a * b) + (b * b))
+  let x = Nat.AlgExp.var(0)
+  let y = Nat.AlgExp.var(1)
+  let exp0 = (x + y) * (x + y)
+  let exp1 = (x * x) + (2 * x * y) + (y * y)
+  Nat.AlgExp.decide(exp0, exp1, a, b)
+

base/Nat/Order.kind

@@ -1,150 +1,246 @@
-Nat.Order.refl(a: Nat): Nat.lte(a, a) == true
+Nat.Order.refl(a: Nat): Equal<Bool>(Nat.lte(a, a), true)
   case a {
     zero:
-      refl
+      Equal.refl<Bool>(true)
     succ:
-      ind = Nat.Order.refl(a.pred)
+      let ind = Nat.Order.refl(a.pred)
       ind
-  }!
+  }: Equal<Bool>(Nat.lte(a, a), true)
 
-Nat.Order.conn(a: Nat, b: Nat): Or<Nat.lte(a, b) == true, Nat.lte(b, a) == true>
-  case a b {
-    zero zero:
-      left(refl)
-    zero succ:
-      left(refl)
-    succ zero:
-      right(refl)
-    succ succ:
-      ind = Nat.Order.conn(a.pred, b.pred)
-      ind
-  }!
+Nat.Order.conn(a: Nat, b: Nat): Or<Equal<Bool>(Nat.lte(a, b), true), Equal<Bool>(Nat.lte(b, a), true)>
+  case a {
+    zero:
+      case b {
+        zero:
+          Either.left<
+            Equal<Bool>(Nat.lte(0, 0), true)
+            Equal<Bool>(Nat.lte(0, 0), true)
+          >(Equal.refl<Bool>(true))
+        succ:
+          Either.left<
+            Equal<Bool>(Nat.lte(0, Nat.succ(b.pred)), true)
+            Equal<Bool>(Nat.lte(Nat.succ(b.pred), 0), true)
+          >(Equal.refl<Bool>(true))
+      }: Or<Equal<Bool>(Nat.lte(0, b), true), Equal<Bool>(Nat.lte(b, 0), true)>
+    succ:
+      case b {
+        zero:
+          Either.right<
+            Equal<Bool>(Nat.lte(Nat.succ(a.pred), 0), true)
+            Equal<Bool>(Nat.lte(0, Nat.succ(a.pred)), true)
+          >(Equal.refl<Bool>(true))
+        succ:
+          let ind = Nat.Order.conn(a.pred, b.pred)
+          ind
+      }: Or<Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), true), Equal<Bool>(Nat.lte(b, Nat.succ(a.pred)), true)>
+  }: Or<Equal<Bool>(Nat.lte(a, b), true), Equal<Bool>(Nat.lte(b, a), true)>
 
 Nat.Order.anti_symm(
   a: Nat
   b: Nat
-  Hyp0: Nat.lte(a, b) == true
-  Hyp1: Nat.lte(b, a) == true
-): a == b
-  case a b with Hyp0 Hyp1 {
-    zero zero:
-      refl
-    zero succ:
-      contra = Bool.true_neq_false(mirror(Hyp1))
-      Empty.absurd!(contra)
-    succ zero:
-      contra = Bool.true_neq_false(mirror(Hyp0))
-      Empty.absurd!(contra)
-    succ succ:
-      ind = Nat.Order.anti_symm(
-        a.pred,
-        b.pred,
-        Hyp0,
-        Hyp1
-      )
-      let qed = apply(Nat.succ, ind)
-      qed
-  }!
+  Hyp0: Equal<Bool>(Nat.lte(a, b), true)
+  Hyp1: Equal<Bool>(Nat.lte(b, a), true)
+): Equal<Nat>(a, b)
+  (case a {
+    zero:
+      (Hyp0, Hyp1)
+        (case b {
+          zero:
+            (Hyp0, Hyp1)
+              Equal.refl<Nat>(0)
+          succ:
+            (Hyp0, Hyp1)
+              let contra = Bool.true_neq_false(
+                Equal.mirror<Bool>(
+                  Nat.lte(Nat.succ(b.pred), 0)
+                  Bool.true
+                  Hyp1
+                )
+              )
+              Empty.absurd<Equal<Nat>(0, Nat.succ(b.pred))>(contra)
+        }: (Hyp0: Equal<Bool>(Nat.lte(0, b), true)) -> (Hyp1: Equal<Bool>(Nat.lte(b, 0), true)) -> Equal<Nat>(0, b))(
+          Hyp0
+          Hyp1
+        )
+    succ:
+      (Hyp0, Hyp1)
+        (case b {
+          zero:
+            (Hyp0, Hyp1)
+              let contra = Bool.true_neq_false(
+                Equal.mirror<Bool>(
+                  Nat.lte(Nat.succ(a.pred), 0)
+                  Bool.true
+                  Hyp0
+                )
+              )
+              Empty.absurd<Equal<Nat>(Nat.succ(a.pred), 0)>(contra)
+          succ:
+            (Hyp0, Hyp1)
+              let ind = Nat.Order.anti_symm(
+                a.pred, b.pred,
+                Hyp0, Hyp1,
+              )
+              let qed = Equal.apply<Nat, Nat>(a.pred, b.pred, Nat.succ, ind)
+              qed
+        }: (Hyp0: Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), true)) ->
+           (Hyp1: Equal<Bool>(Nat.lte(b, Nat.succ(a.pred)), true)) ->
+           Equal<Nat>(Nat.succ(a.pred), b))(
+          Hyp0
+          Hyp1
+        )
+  }: (Hyp0: Equal<Bool>(Nat.lte(a, b), true)) -> (Hyp1: Equal<Bool>(Nat.lte(b, a), true)) -> Equal<Nat>(a, b))(
+    Hyp0
+    Hyp1
+  )
 
 Nat.Order.chain.aux(
   a: Nat
-  Hyp: Nat.lte(a, 0) == true
-): a == 0
-  case a with Hyp {
-    zero: refl
-    succ: contra = Bool.true_neq_false(mirror(Hyp))
-          Empty.absurd!(contra)
-  }!
+  Hyp: Equal<Bool>(Nat.lte(a, 0), true)
+): Equal<Nat>(a, 0)
+  (case a {
+    zero:
+      (Hyp)
+        Equal.refl<Nat>(0)
+    succ:
+      (Hyp)
+        let contra = Bool.false_neq_true(Hyp)
+        Empty.absurd<Equal<Nat>(Nat.succ(a.pred), 0)>(contra)
+  }: (Hyp: Equal<Bool>(Nat.lte(a, 0), true)) -> Equal<Nat>(a, 0))(
+    Hyp
+  )
 
 Nat.Order.chain(
   a: Nat
   b: Nat
   c: Nat
-  Hyp0: Nat.lte(a, b) == true
-  Hyp1: Nat.lte(b, c) == true
-): Nat.lte(a, c) == true
-  case b with Hyp0 Hyp1 {
+  Hyp0: Equal<Bool>(Nat.lte(a, b), true)
+  Hyp1: Equal<Bool>(Nat.lte(b, c), true)
+): Equal<Bool>(Nat.lte(a, c), true)
+  (case b {
     zero:
-      a_zero = mirror(Nat.Order.chain.aux(a, Hyp0))
-      qed = Hyp1 :: rewrite X in Nat.lte(X, _) == _ with a_zero
-      qed
+      (Hyp0, Hyp1)
+        let a_zero = Equal.mirror<Nat>(a, 0, Nat.Order.chain.aux(a, Hyp0))
+        let qed = Equal.rewrite<Nat>(0, a, a_zero, (x) Equal<Bool>(Nat.lte(x, c), true), Hyp1)
+        qed
     succ:
-      case a with Hyp0 Hyp1 {
-        zero:
-          refl
-        succ:
-          case c with Hyp0 Hyp1 {
-            zero:
-              b_zero = Nat.Order.chain.aux(Nat.succ(b.pred), Hyp1)
-              contra = Nat.succ_neq_zero!(b_zero)
-              Empty.absurd!(contra)
-            succ:
-              ind = Nat.Order.chain(a.pred, b.pred, c.pred, Hyp0, Hyp1)
-              ind
-          }!
-      }!
-  }!
+      (Hyp0, Hyp1)
+        (case a {
+          zero:
+            (Hyp0, Hyp1)
+              Equal.refl<Bool>(true)
+          succ:
+            (Hyp0, Hyp1)
+              (case c {
+                zero:
+                  (Hyp0, Hyp1)
+                    let b_zero = Nat.Order.chain.aux(Nat.succ(b.pred), Hyp1)
+                    let contra = Nat.succ_neq_zero(b.pred, b_zero)
+                    Empty.absurd(Equal<Bool>(Nat.lte(Nat.succ(a.pred), 0), true), contra)
+                succ:
+                  (Hyp0, Hyp1)
+                    let ind = Nat.Order.chain(a.pred, b.pred, c.pred, Hyp0, Hyp1)
+                    ind
+              }:
+                (Hyp0: Equal<Bool>(Nat.lte(Nat.succ(a.pred), Nat.succ(b.pred)), true)) ->
+                (Hyp1: Equal<Bool>(Nat.lte(Nat.succ(b.pred), c), true)) ->
+                Equal<Bool>(Nat.lte(Nat.succ(a.pred), c), true))(
+                  Hyp0
+                  Hyp1
+                )
+        }:
+          (Hyp0: Equal<Bool>(Nat.lte(a, Nat.succ(b.pred)), true)) ->
+          (Hyp1: Equal<Bool>(Nat.lte(Nat.succ(b.pred), c), true)) ->
+          Equal<Bool>(Nat.lte(a, c), true))(
+            Hyp0
+            Hyp1
+          )
+  }: (Hyp0: Equal<Bool>(Nat.lte(a, b), true), Hyp1: Equal<Bool>(Nat.lte(b, c), true)) -> Equal<Bool>(Nat.lte(a, c), true))(
+    Hyp0
+    Hyp1
+  )
 
 Nat.Order.add.left(
   a: Nat
   b: Nat
   c: Nat
-  Hyp: Nat.lte(a, b) == true
-): Nat.lte(c + a, c + b) == true
-  case c {
+  Hyp: Equal<Bool>(Nat.lte(a, b), true)
+): Equal<Bool>(Nat.lte(Nat.add(c, a), Nat.add(c, b)), true)
+  (case c {
     zero:
-      Hyp
+      (Hyp)
+        Hyp
     succ:
-      Nat.Order.add.left(a, b, c.pred, Hyp)
-  }!
+      (Hyp)
+        Nat.Order.add.left(a, b, c.pred, Hyp)
+  }:
+    (Hyp: Equal<Bool>(Nat.lte(a, b), true)) ->
+    Equal<Bool>(Nat.lte(Nat.add(c, a), Nat.add(c, b)), true))(
+      Hyp
+    )
 
 Nat.Order.add.right(
   a: Nat
   b: Nat
   c: Nat
-  Hyp: Nat.lte(a, b) == true
-): Nat.lte(a + c, b + c) == true
-  (Nat.Order.add.left!!(c, Hyp)
-    :: rewrite X in Nat.lte(X, _) == _ with Nat.add.comm!!)
-    :: rewrite X in Nat.lte(_, X) == _ with Nat.add.comm!!
+  Hyp: Equal<Bool>(Nat.lte(a, b), true)
+): Equal<Bool>(Nat.lte(Nat.add(a, c), Nat.add(b, c)), true)
+  let lem = Nat.Order.add.left(a, b, c, Hyp)
+  let lem = Equal.rewrite<Nat>(
+    Nat.add(c, a), Nat.add(a, c), Nat.add.comm(c, a),
+    (x) Equal<Bool>(Nat.lte(x, Nat.add(c, b)), true), lem
+  )
+  let qed = Equal.rewrite<Nat>(
+    Nat.add(c, b), Nat.add(b, c), Nat.add.comm(c, b),
+    (x) Equal<Bool>(Nat.lte(Nat.add(a, c), x), true), lem
+  )
+  qed
 
 Nat.Order.add.combine(
   a: Nat
   b: Nat
   c: Nat
   d: Nat
-  Hyp0: Nat.lte(a, b) == true
-  Hyp1: Nat.lte(c, d) == true
-): Nat.lte(a + c, b + d) == true
-  left_lem = Nat.Order.add.right!!(c, Hyp0)
-  right_lem = Nat.Order.add.left!!(b, Hyp1)
-  qed = Nat.Order.chain!!!(left_lem, right_lem)
+  Hyp0: Equal<Bool>(Nat.lte(a, b), true)
+  Hyp1: Equal<Bool>(Nat.lte(c, d), true)
+): Equal<Bool>(Nat.lte(Nat.add(a, c), Nat.add(b, d)), true)
+  let left_lem = Nat.Order.add.right(a, b, c, Hyp0)
+  let right_lem = Nat.Order.add.left(c, d, b, Hyp1)
+  let qed = Nat.Order.chain(Nat.add(a, c), Nat.add(b, c), Nat.add(b,d), left_lem, right_lem)
   qed
 
-Nat.Order.mul.right(
-  a: Nat
-  b: Nat
-  c: Nat
-  Hyp: Nat.lte(a, b) == true
-): Nat.lte(Nat.mul(a, c), Nat.mul(b, c)) == true
-  c(
-    (c) Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true),
-    refl,
-    (c.pred)
-      let ind = Nat.Order.mul.right(a, b, c.pred, Hyp)
-      let qed = Nat.Order.add.combine(a, b, Nat.mul(a,c.pred), Nat.mul(b,c.pred), Hyp, ind)
-      qed
-   )
-
 Nat.Order.mul.left(
   a: Nat
   b: Nat
   c: Nat
   Hyp: Equal<Bool>(Nat.lte(a, b), Bool.true)
 ): Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), Bool.true)
-  lem = Nat.Order.mul.right(a, b, c, Hyp)
-  lem = lem :: rewrite X in Nat.lte(X, Nat.mul(b, c)) == true with Nat.mul.comm(a, c)
-  qed = lem :: rewrite X in Nat.lte(Nat.mul(c, a), X) == true with Nat.mul.comm(b, c)
+  // TODO
+  case c {
+    zero:
+      Equal.refl<Bool>(true)
+    succ:
+      let ind = Nat.Order.mul.left(a, b, c.pred, Hyp)
+      let qed = Nat.Order.add.combine(a, b, Nat.mul(c.pred,a),Nat.mul(c.pred,b), Hyp, ind)
+      qed
+  }: Equal<Bool>(Nat.lte(Nat.mul(c, a), Nat.mul(c, b)), true)
+
+
+Nat.Order.mul.right(
+  a: Nat
+  b: Nat
+  c: Nat
+  Hyp: Equal<Bool>(Nat.lte(a, b), true)
+): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, c)), true)
+  let lem = Nat.Order.mul.left(a, b, c, Hyp)
+  let lem = Equal.rewrite<Nat>(
+    Nat.mul(c,a), Nat.mul(a, c), Nat.mul.comm(c, a)
+    (x) Equal<Bool>(Nat.lte(x, Nat.mul(c, b)), Bool.true), lem
+  )
+  let qed = Equal.rewrite<Nat>(
+    Nat.mul(c, b), Nat.mul(b, c), Nat.mul.comm(c, b)
+    (x) Equal<Bool>(Nat.lte(Nat.mul(a, c), x), Bool.true), lem
+  )
   qed
 
 Nat.Order.mul.combine(
@@ -155,9 +251,9 @@ Nat.Order.mul.combine(
   Hyp0: Equal<Bool>(Nat.lte(a, b), Bool.true),
   Hyp1: Equal<Bool>(Nat.lte(c, d), Bool.true)
 ): Equal<Bool>(Nat.lte(Nat.mul(a, c), Nat.mul(b, d)), Bool.true)
-  let left_lem = Nat.Order.mul.right(a, b, c, Hyp0);
-  let right_lem = Nat.Order.mul.left(c, d, b, Hyp1);
-  let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem);
+  let left_lem = Nat.Order.mul.right(a, b, c, Hyp0)
+  let right_lem = Nat.Order.mul.left(c, d, b, Hyp1)
+  let qed = Nat.Order.chain(Nat.mul(a, c), Nat.mul(b, c), Nat.mul(b, d), left_lem, right_lem)
   qed
 
 //Nat.Order.bernoulli(

base/Nat/add/assoc.kind

@@ -1,8 +1,13 @@
-Nat.add.assoc(a: Nat, b: Nat, c: Nat)
- : ((a + b) + c) == a + (b + c)
- case a{
-   zero: refl
+Nat.add.assoc(
+  a: Nat, b: Nat, c: Nat
+): Equal<Nat>(Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)))
+ case a {
+   zero:
+     Equal.refl<Nat>(Nat.add(b, c))
    succ: 
-    let h=Nat.add.assoc(a.pred, b, c)
-    Equal.apply!!<Nat.add(Nat.add(a.pred,b),c), Nat.add(a.pred,Nat.add(b,c)),Nat.succ>(h)
+    let h = Nat.add.assoc(a.pred, b, c)
+    Equal.apply<Nat, Nat>(
+      Nat.add(Nat.add(a.pred,b),c), Nat.add(a.pred,Nat.add(b,c)),
+      Nat.succ, h
+    )
  }!

base/Nat/add/cancel_left.kind

@@ -1,9 +1,22 @@
-Nat.add.cancel_left(a: Nat, b: Nat, c: Nat, e0: (a + b) == a + c): b == c
-  case a with e0 {
-    zero: e0
+Nat.add.cancel_left(a: Nat, b: Nat, c: Nat, e0: Equal<Nat>(Nat.add(a, b), Nat.add(a, c))): Equal<Nat>(b, c)
+  (case a {
+    zero:
+      (e0)
+        e0
     succ: 
-      let e2 = e0 :: rewrite x in x == _ with Nat.add.succ_left(a.pred, b) 
-      let e3 = e2 :: rewrite x in _ == x with Nat.add.succ_left(a.pred, c)
-      let e4 = Nat.succ_inj!!(e3)
-      Nat.add.cancel_left!!!(e4)
-  }!
+      (e0)
+        let e2 = Equal.rewrite<Nat>(
+          Nat.add(Nat.succ(a.pred),b), Nat.succ(Nat.add(a.pred,b)),
+          Nat.add.succ_left(a.pred, b),
+          (x) Equal<Nat>(x, Nat.add(Nat.succ(a.pred),c)), e0
+        )
+        let e3 = Equal.rewrite<Nat>(
+          Nat.add(Nat.succ(a.pred),c), Nat.succ(Nat.add(a.pred,c))
+          Nat.add.succ_left(a.pred, c)
+          (x) Equal<Nat>(Nat.succ(Nat.add(a.pred,b)), x), e2
+        )
+        let e4 = Nat.succ_inj(Nat.add(a.pred,b), Nat.add(a.pred,c), e3)
+        Nat.add.cancel_left(a.pred, b, c, e4)
+  }: (e0: Equal<Nat>(Nat.add(a, b), Nat.add(a, c))) -> Equal<Nat>(b, c))(
+    e0
+  )

base/Nat/add/cancel_right.kind

@@ -1,6 +1,16 @@
 // if a + b == c + b, then a == c. 
-Nat.add.cancel_right(a: Nat, b: Nat, c: Nat, h: (a + b) == c + b)
-  : a == c
-  let h1 = h :: rewrite x in x == Nat.add(c,b) with Nat.add.comm(a, b)
-  let h2 = h1:: rewrite x in Nat.add(b,a) == x with Nat.add.comm(c, b)
-  Nat.add.cancel_left(_ _ _ h2)
+Nat.add.cancel_right(
+  a: Nat, b: Nat, c: Nat, h: Equal<Nat>(Nat.add(a, b), Nat.add(c, b))
+): Equal<Nat>(a, c)
+  let lemma = Equal.rewrite<Nat>(
+    Nat.add(a,b), Nat.add(b,a), Nat.add.comm(a, b),
+    (x) Equal<Nat>(x, Nat.add(c, b))
+    h
+  )
+  let lemma = Equal.rewrite<Nat>(
+    Nat.add(c,b), Nat.add(b,c), Nat.add.comm(c, b),
+    (x) Equal<Nat>(Nat.add(b, a), x)
+    lemma
+  )
+  let qed = Nat.add.cancel_left(b, a, c, lemma)
+  qed

base/Nat/add/comm.kind

@@ -1,13 +1,26 @@
-Nat.add.comm(a: Nat, b:Nat): (a + b) == (b + a)
-  case a{
-    zero: mirror(Nat.add.zero_right(b))
+Nat.add.comm(
+  a: Nat, b:Nat
+): Equal<Nat>(Nat.add(a, b), Nat.add(b, a))
+  case a {
+    zero:
+      Equal.mirror<Nat>(
+        Nat.add(b,0), b
+        Nat.add.zero_right(b)
+      )
     succ: 
-      let p0 = Nat.add.succ_right(b, a.pred)
-      let p1 = mirror(p0)
-      let h2 = Nat.add.comm(b, a.pred)
-      let p3 = p1 :: rewrite x in Nat.succ(x) == Nat.add(b,Nat.succ(a.pred)) with h2
-      // here p3 should close the goal.
-      let p4 = mirror(Nat.add.succ_left(a.pred,b))
-      let p5 = p3 :: rewrite x in x == _ with p4
-      p5
-  }!
+      let ind = Nat.add.comm(a.pred, b)
+      let lemma = Equal.apply<Nat, Nat>(
+        Nat.add(a.pred,b), Nat.add(b,a.pred)
+        Nat.succ, ind
+      )
+      let succ_right = Equal.mirror<Nat>(
+        Nat.add(b,Nat.succ(a.pred)), Nat.succ(Nat.add(b,a.pred))
+        Nat.add.succ_right(b, a.pred)
+      )
+      let qed = Equal.rewrite<Nat>(
+        Nat.succ(Nat.add(b,a.pred)), Nat.add(b,Nat.succ(a.pred)), succ_right
+        (x) Equal<Nat>(Nat.add(Nat.succ(a.pred), b), x)
+        lemma
+      )
+      qed
+  }: Equal<Nat>(Nat.add(a, b), Nat.add(b, a))

base/Nat/add/succ_both.kind

@@ -1,5 +1,6 @@
-Nat.add.succ_both(a: Nat, b: Nat)
-: (Nat.succ(a) + Nat.succ(b)) == Nat.succ(Nat.succ(a + b))
+Nat.add.succ_both(
+  a: Nat, b: Nat
+): (Nat.succ(a) + Nat.succ(b)) == Nat.succ(Nat.succ(a + b))
   case a {
     zero: refl
     succ: apply(Nat.succ, Nat.add.succ_both(a.pred, b))

base/Nat/mul.kind

@@ -1,5 +1,7 @@
 Nat.mul(n: Nat, m: Nat): Nat
-  case m {
-    zero: Nat.zero,
-    succ: Nat.add(n, Nat.mul(n, m.pred)),
-  }
+  case n {
+    zero:
+      0
+    succ:
+      Nat.add(m, Nat.mul(n.pred, m))
+  }

base/Nat/mul/assoc.kind

@@ -1,8 +1,32 @@
-Nat.mul.assoc(a: Nat, b: Nat, c: Nat): (a * b * c) == (a * b) * c
-  case c{
-    zero: refl
-    succ: 
-      let begin = Equal.refl<_, (a * b) + (a * (b * c.pred))>
-      let second = begin :: rewrite x in x == (a * b) + (a * (b * c.pred)) with mirror(Nat.mul.distrib_left(a, b, b * c.pred))
-      second :: rewrite x in _ == (a * b) + x with Nat.mul.assoc(a,b,c.pred)
-  }!
+Nat.mul.assoc(
+  a: Nat, b: Nat, c: Nat
+): Equal<Nat>(Nat.mul(a, Nat.mul(b, c)), Nat.mul(Nat.mul(a, b), c))
+  case a {
+    zero:
+      Equal.refl<Nat>(0)
+    succ:
+      let ind = Nat.mul.assoc(a.pred, b, c)
+      let lemma = Equal.apply<Nat, Nat>(
+        Nat.mul(a.pred,Nat.mul(b,c)), Nat.mul(Nat.mul(a.pred,b),c), Nat.add(Nat.mul(b, c))
+        ind
+      )
+      let distrib = Equal.mirror<Nat>(
+        Nat.mul(Nat.add(b,Nat.mul(a.pred,b)),c), Nat.add(Nat.mul(b,c),Nat.mul(Nat.mul(a.pred,b),c))
+        Nat.mul.distrib_right(b, Nat.mul(a.pred, b), c)
+      )
+      let qed = Equal.rewrite<Nat>(
+        Nat.add(Nat.mul(b,c),Nat.mul(Nat.mul(a.pred,b),c))
+        Nat.mul(Nat.add(b,Nat.mul(a.pred,b)),c)
+        distrib,
+        (x) Equal<Nat>(Nat.add(Nat.mul(b,c),Nat.mul(a.pred,Nat.mul(b,c))), x)
+        lemma
+      )
+      qed
+  }: Equal<Nat>(Nat.mul(a, Nat.mul(b, c)), Nat.mul(Nat.mul(a, b), c))
+
+// induction on a
+// - ind:             a.pred * b * c  ==            (a.pred * b) * c  ok
+//         (b * c) + (a.pred * b * c) == (b * c) + ((a.pred * b) * c) ok
+//         (b * c) + (a.pred * b * c) == (b + a.pred * b) * c
+//         succ(a.pred) * b * c == (succ(a.pred) * b) * c
+// - goal: succ(a.pred) * b * c == (succ(a.pred) * b) * c

base/Nat/mul/comm.kind

@@ -1,5 +1,24 @@
-Nat.mul.comm(a: Nat, b: Nat): (a * b) == b * a
-  case b {
-    zero: mirror(Nat.mul.zero_left(a))
-    succ: mirror(Nat.mul.comm(Nat.succ(b.pred), a))
-  }!
+Nat.mul.comm(a: Nat, b: Nat): Equal<Nat>(Nat.mul(a, b), Nat.mul(b, a))
+  case a {
+    zero:
+      Equal.mirror<Nat>(Nat.mul(b, 0), 0, Nat.mul.zero_right(b))
+    succ:
+      let ind = Nat.mul.comm(a.pred, b)
+      let lemma = Equal.apply<Nat, Nat>(
+        Nat.mul(a.pred,b), Nat.mul(b,a.pred)
+        Nat.add(b), ind
+      )
+      let succ_right = mirror(Nat.mul.succ_right(b, a.pred))
+      let qed = Equal.rewrite<Nat>(
+        Nat.add(b,Nat.mul(b,a.pred)), Nat.mul(b,Nat.succ(a.pred))
+        succ_right,
+        (x) Equal<Nat>(Nat.add(b,Nat.mul(a.pred,b)), x)
+        lemma
+      )
+      qed
+  }: Equal<Nat>(Nat.mul(a, b), Nat.mul(b, a))
+
+// ind:        a.pred * b == b * a.pred
+//       b + a.pred * b == b + b * a.pred
+//       b + a.pred * b == b * succ(a.pred)
+// goal: succ(a.pred) * b == b * succ(a.pred)

base/Nat/mul/distrib_left.kind

@@ -1,11 +1,21 @@
-Nat.mul.distrib_left(a: Nat, b: Nat, c: Nat):
-  (a * (b + c)) == ((a * b) + (a * c))
-  case b{
-    zero: refl 
-    succ: 
-      let final = Equal.refl<_, (a + (a * b.pred)) + (a * c)>
-      let final2 = final :: rewrite x in x == (a + (a * b.pred)) + (a * c) with Nat.add.assoc(a, a * b.pred, a * c)
-      let f = final2 :: rewrite x in (a + x) == (a + (a * b.pred)) + (a*c) with mirror(Nat.mul.distrib_left(a, b.pred, c))
-      f
-  }!
-  
+Nat.mul.distrib_left(
+  a: Nat, b: Nat, c: Nat
+): Equal<Nat>(Nat.mul(a, Nat.add(b, c)), Nat.add(Nat.mul(a, b), Nat.mul(a, c)))
+  let lemma = Nat.mul.distrib_right(b, c, a)
+  let lemma = Equal.rewrite<Nat>(
+    Nat.mul(Nat.add(b, c), a), Nat.mul(a, Nat.add(b, c))
+    Nat.mul.comm(Nat.add(b, c), a)
+    (x) Equal<Nat>(x, Nat.add(Nat.mul(b,a),Nat.mul(c,a)))
+    lemma
+  )
+  let lemma = Equal.rewrite<Nat>(
+    Nat.mul(b, a), Nat.mul(a, b), Nat.mul.comm(b, a)
+    (x) Equal<Nat>(Nat.mul(a,Nat.add(b,c)), Nat.add(x, Nat.mul(c,a)))
+    lemma
+  )
+  let qed = Equal.rewrite<Nat>(
+    Nat.mul(c, a), Nat.mul(a, c), Nat.mul.comm(c, a)
+    (x) Equal<Nat>(Nat.mul(a, Nat.add(b,c)), Nat.add(Nat.mul(a, b), x))
+    lemma
+  )
+  qed

base/Nat/mul/distrib_right.kind

@@ -0,0 +1,27 @@
+Nat.mul.distrib_right(
+  a: Nat, b: Nat, c: Nat
+): Equal<Nat>(Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c)))
+  case a {
+    zero:
+      Equal.refl<Nat>(Nat.mul(b, c))
+    succ:
+      // ind:       (a.pred + b) * c == (a.pred * c) + (b * c)
+      // lemma: c + (a.pred + b) * c ==  c + (a.pred * c)  + (b * c)
+      // qed:   c + (a.pred + b) * c == (c + (a.pred * c)) + (b * c)
+      let ind = Nat.mul.distrib_right(
+        a.pred, b, c
+      )
+      let lemma = Equal.apply<Nat, Nat>(
+        Nat.mul(Nat.add(a.pred,b),c), Nat.add(Nat.mul(a.pred,c),Nat.mul(b,c)), Nat.add(c), ind
+      )
+      let assoc = Equal.mirror<Nat>(
+        Nat.add(Nat.add(c,Nat.mul(a.pred,c)),Nat.mul(b,c)), Nat.add(c,Nat.add(Nat.mul(a.pred,c),Nat.mul(b,c)))
+        Nat.add.assoc(c, Nat.mul(a.pred, c), Nat.mul(b, c))
+      )
+      let qed = Equal.rewrite<Nat>(
+        Nat.add(c,Nat.add(Nat.mul(a.pred,c),Nat.mul(b,c))), Nat.add(Nat.add(c,Nat.mul(a.pred,c)),Nat.mul(b,c)), assoc,
+        (x) Equal<Nat>(Nat.add(c, Nat.mul(Nat.add(a.pred, b), c)), x)
+        lemma
+      )
+      qed
+  }: Equal<Nat>(Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c)))

base/Nat/mul/one_left.kind

@@ -1,7 +1,2 @@
-Nat.mul.one_left(a: Nat): (1 * a) == a
-  case a{
-    zero: refl
-    succ: 
-      let h = Nat.mul.one_left(a.pred)
-      Equal.apply!!<Nat.mul(1,a.pred),a.pred,Nat.succ>(h)
-  }!
+Nat.mul.one_left(a: Nat): Equal<Nat>(Nat.mul(1, a), a)
+  Nat.add.zero_right(a)

base/Nat/mul/one_right.kind

@@ -1,2 +1,11 @@
-Nat.mul.one_right(a: Nat): (a * 1) == a
-  Nat.add.zero_right(a)
+Nat.mul.one_right(a: Nat): Equal<Nat>(Nat.mul(a, 1), a)
+  case a {
+    zero:
+      Equal.refl<Nat>(0)
+    succ:
+      let ind = Nat.mul.one_right(a.pred)
+      let qed = Equal.apply<Nat, Nat>(
+        Nat.mul(a.pred, 1), a.pred, Nat.succ, ind
+      )
+      qed
+  }: Equal<Nat>(Nat.mul(a, 1), a)

base/Nat/mul/succ_left.kind

@@ -1,7 +1,2 @@
-// FIXME: this proof isn't working as written anymore
-Nat.mul.succ_left(a: Nat, b: Nat): (Nat.succ(a) * b) == b + (a * b)
-  Nat.mul.succ_left(a, b)
-  //let h = Nat.mul.succ_right(b,a)
-  //let left = h :: rewrite x in x == _ with Nat.mul.comm(_ _)
-  //let final = left :: rewrite x in _ == Nat.add(b,x) with Nat.mul.comm(_ _)
-  //final
+Nat.mul.succ_left(a: Nat, b: Nat): Equal<Nat>(Nat.mul(Nat.succ(a), b), Nat.add(b, Nat.mul(a, b)))
+  Equal.refl<Nat>(Nat.mul(Nat.succ(a), b))

base/Nat/mul/succ_right.kind

@@ -1,3 +1,42 @@
-Nat.mul.succ_right(a: Nat, b: Nat)
-: (a * Nat.succ(b)) == a + (a * b)
-  refl
+Nat.mul.succ_right(
+  a: Nat, b: Nat
+): Equal<Nat>(Nat.mul(a, Nat.succ(b)), Nat.add(a, Nat.mul(a, b)))
+  case a {
+    zero:
+      Equal.refl<Nat>(0)
+    succ:
+      let ind = Nat.mul.succ_right(a.pred, b)
+      let lemma = Equal.apply<Nat, Nat>(
+        Nat.mul(a.pred,Nat.succ(b)), Nat.add(a.pred, Nat.mul(a.pred, b)),
+        (x) Nat.add(b, x), ind
+      )
+      let assoc_to = 
+        Equal.mirror<Nat>(
+          Nat.add(Nat.add(b, a.pred), Nat.mul(a.pred, b)), Nat.add(b, Nat.add(a.pred, Nat.mul(a.pred, b))),
+          Nat.add.assoc(b, a.pred, Nat.mul(a.pred, b))
+        )
+      let lemma = Equal.rewrite<Nat>(
+        Nat.add(b, Nat.add(a.pred, Nat.mul(a.pred,b))), Nat.add(Nat.add(b, a.pred),Nat.mul(a.pred,b)),
+        assoc_to,
+        (x) Equal<Nat>(Nat.add(b, Nat.mul(a.pred, Nat.succ(b))), x),
+        lemma
+      )
+      let lemma = Equal.rewrite<Nat>(
+        Nat.add(b, a.pred), Nat.add(a.pred, b),
+        Nat.add.comm(b, a.pred),
+        (x) Equal<Nat>(Nat.add(b, Nat.mul(a.pred, Nat.succ(b))), Nat.add(x,Nat.mul(a.pred,b))),
+        lemma
+      )
+      let assoc_back = Nat.add.assoc(a.pred, b, Nat.mul(a.pred, b))
+      let lemma = Equal.rewrite<Nat>(
+        Nat.add(Nat.add(a.pred, b),Nat.mul(a.pred,b)), Nat.add(a.pred, Nat.add(b, Nat.mul(a.pred,b))),
+        assoc_back,
+        (x) Equal<Nat>(Nat.add(b, Nat.mul(a.pred, Nat.succ(b))), x),
+        lemma
+      )
+      let qed = Equal.apply<Nat, Nat>(
+        Nat.add(b,Nat.mul(a.pred,Nat.succ(b))), Nat.add(a.pred,Nat.add(b,Nat.mul(a.pred,b))),
+        Nat.succ, lemma
+      )
+      qed
+  }: Equal<Nat>(Nat.mul(a, Nat.succ(b)), Nat.add(a, Nat.mul(a, b)))

base/Nat/mul/zero_left.kind

@@ -1,7 +1,8 @@
-Nat.mul.zero_left(a: Nat): (0 * a) == 0
-  case a{
-    zero: refl
+Nat.mul.zero_left(a: Nat): Equal<Nat>(Nat.mul(0, a), 0)
+  case a {
+    zero:
+      Equal.refl<Nat>(0)
     succ: 
       let h = Nat.mul.zero_left(a.pred)
-      apply((x) (0+x), h)
-  }!
+      h
+  }: Equal<Nat>(Nat.mul(0, a), 0)

base/Nat/mul/zero_right.kind

@@ -1,2 +1,7 @@
-Nat.mul.zero_right(a: Nat): (a * 0) == 0
-  refl
+Nat.mul.zero_right(a: Nat): Equal<Nat>(Nat.mul(a, 0), 0)
+  case a {
+    zero:
+      Equal.refl<Nat>(0)
+    succ:
+      Nat.mul.zero_right(a.pred)
+  }: Equal<Nat>(Nat.mul(a, 0), 0)

base/Nat/succ_neq_zero.kind

@@ -1,2 +1,2 @@
 Nat.succ_neq_zero(a: Nat): Not(Equal<Nat, Nat.succ(a), 0>)
-  (e) Bool.false_neq_true(apply(Nat.is_zero, e))
+  (e) Bool.false_neq_true(Equal.apply<Nat, Bool>(Nat.succ(a), 0, Nat.is_zero, e))