diff --git a/base/RLP.kind b/base/RLP.kind
index 32ab937d..7f2edb7e 100644
--- a/base/RLP.kind
+++ b/base/RLP.kind
@@ -79,7 +79,7 @@ RLP.encode.many(trees: List<RLP>): Bytes
 RLP.encode(tree: RLP): Bytes
   case tree {
     data:
-      if Bool.and(Nat.eql(List.length!(tree.value),1), U8.ltn(List.head_with_default!(0#8,tree.value), 128#8)) then
+      if Bool.and(Nat.eql(List.length!(tree.value),1), Nat.ltn(U8.to_nat((List.head_with_default!(0#8,tree.value))), 128)) then
         tree.value
       else
         List.concat!(RLP.encode.length(128, List.length!(tree.value)), tree.value)
diff --git a/base/RLP/aux.kind b/base/RLP/aux.kind
index 259e9915..f0469af4 100644
--- a/base/RLP/aux.kind
+++ b/base/RLP/aux.kind
@@ -1,10 +1,14 @@
+because_i_said_so<A: Type>: A
+  because_i_said_so<A>
+
 // These sub-theorems were not proven yet!
 // Most of them are simple, and should be finished over the next days
-//RLP.aux.split.0(
-//  payload: Bytes
-//  tail: Bytes
-//  H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
-//): RLP.split.length(128, RLP.encode.length(128, List.length<U8>(payload)) ++ payload ++ tail) == {payload, tail}
+RLP.aux.split.0(
+  payload: Bytes
+  tail: Bytes
+  H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
+): Pair.new(Bytes, Bytes, payload, tail) == RLP.split.length(128, Nat.to_u8(Nat.add(128, List.length!(payload))) & payload ++ tail)
+  because_i_said_so!
 //  let H = mirror(H)
 //  case H {
 //    refl:
@@ -19,6 +23,23 @@
 //  }: RLP.split.length(128,List.concat(U8,  H.b(  () Bytes,List.cons(U8,Nat.to_u8(Nat.add(128,List.length(U8,payload))),List.nil(U8)),List.concat(U8,Bytes.from_nat(Nat.add(56,Nat.add(128,RLP.needed_bytes(List.length(U8,payload))))),Bytes.from_nat(List.length(U8,payload)))),List.concat(U8,payload,tail))) == Pair.new(Bytes,Bytes,payload,tail)
 
 RLP.aux.split.1(
+  payload: Bytes
+  tail: Bytes
+  H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
+): Pair.new(Bytes, Bytes, payload, tail) ==
+     let b = Bytes.from_nat(List.length!(payload))
+     let a = Nat.to_u8(Nat.add(56, Nat.add(128, List.length!(b))))
+     RLP.split.length(192, a & (b ++ payload) ++ tail)
+  because_i_said_so!
+
+RLP.aux.split.2(
+  payload: Bytes
+  tail: Bytes
+  H: Equal<Bool>(Nat.lte(List.length!(payload), 55), true)
+): Pair.new(Bytes, Bytes, payload, tail) == RLP.split.length(192, Nat.to_u8(Nat.add(192, List.length!(payload))) & payload ++ tail)
+  because_i_said_so!
+
+RLP.aux.split.3(
   payload: Bytes
   tail: Bytes
   H1: Equal<Bool>(Nat.lte(List.length!(payload), 55), false)
@@ -27,7 +48,7 @@ RLP.aux.split.1(
      let b = Bytes.from_nat(List.length!(payload))
      let a = Nat.to_u8(Nat.add(56, Nat.add(192, List.length!(b))))
      RLP.split.length(192, a & (b ++ payload) ++ tail)
-  RLP.aux.split.1(payload, tail, H1, H0)
+  because_i_said_so!
 // let H1 = mirror(H1)
 // case H1 {
 //   refl:
diff --git a/base/RLP/encode_identity.kind b/base/RLP/encode_identity.kind
index 80568aba..079c066f 100644
--- a/base/RLP/encode_identity.kind
+++ b/base/RLP/encode_identity.kind
@@ -1,6 +1,9 @@
 typeof<A: Type>(a: A): Type
   A
 
+because_i_said_so<A: Type>: A
+  because_i_said_so<A>
+
 RLP.encode_identity(
   rlps: List<RLP>
   H: Equal<Bool>(Nat.lte(List.length(U8, RLP.encode.many(rlps)), RLP.max), true)
@@ -11,62 +14,83 @@ RLP.encode_identity(
     cons:
       case rlps.head {
         data:
-          ?data
-        node:
-          let ind = RLP.encode_identity(rlps.head.child, ?todo.0)
-          case Nat.lte(List.length(U8,RLP.encode.many(rlps.head.child)), 55) {
+          let split_conditions = Bool.and.split(Nat.eql(List.length!(rlps.head.value),1), Nat.ltn(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 128))
+          case Bool.and(Nat.eql(List.length!(rlps.head.value),1), Nat.ltn(U8.to_nat((List.head_with_default!(0#8,rlps.head.value))), 128)) with split_conditions {
             true:
-              ?true-1110-
+              use conditions = split_conditions(refl)
+              ?true
             false:
-              let recover_prefix = ?todo.1 :: Nat.add(248, List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))) == U8.to_nat(Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))))
-              case recover_prefix {
-                refl:
-                  let lemma = RLP.aux.split.1(RLP.encode.many(rlps.head.child), RLP.encode.many(rlps.tail), ?todo.2, ?todo.3)
-                  case lemma {
-                    refl:
-                      let ind_right = RLP.encode_identity(rlps.tail, ?todo.4)
-                      let ind_left  = RLP.encode_identity(rlps.head.child, ?todo.5)
-                      ?test-258
-                  }: lemma.b( () List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
-
-              }: Nat.lte(    recover_prefix.b,    127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail)))),Nat.lte(    recover_prefix.b    ,191,() List(RLP),RLP.split.length(128,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
-
-              //?false-1110-278-70-10
-
-          }: RLP.decode.many(List.concat(U8,List.concat(U8,    self(    () Bytes,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
+              ?false
+          }!
+          //?data-22-86-
+//          let remember = Equal.refl(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)))
+//          case Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)) as X
+//                with remember : Equal(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)), X)
+//           {
+//            true : 
+//              let break_and1 = RLP.aux.10!!(remember)
+//              let break_and2 = RLP.aux.11!!(remember)
+//              let ensure_non_empty = RLP.aux.12(rlp.value, break_and1)
+//              replace X with mirror(ensure_non_empty) in Maybe.default(RLP,List.head(RLP,X((bytes) List(RLP),List.nil(RLP),(bytes.head) (bytes.tail) U8.ltn(bytes.head,Nat.to_u8(128),() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,bytes.head,List.nil(U8))),RLP.decode.many(bytes.tail)),U8.ltn(bytes.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
+//              replace X with mirror(break_and2) in Maybe.default(RLP,List.head(RLP,X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),rlp.value),List.nil(U8))),RLP.decode.many(List.nil(U8))),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
+//              let list_length_1 = RlP.new_aux.list_length_1_identity(U8, rlp.value, Nat.to_u8(0), break_and1)
+//              replace X with mirror(list_length_1) in RLP.data(X) == RLP.data(rlp.value)
+//              refl
+//            false : 
+//              let list_u8 = Equal.refl<Bytes, RLP.encode.length(128,List.length(U8,rlp.value))>
+//              case RLP.encode.length(128,List.length(U8,rlp.value)) as X with list_u8 : Equal(Bytes, RLP.encode.length(128,List.length(U8,rlp.value)), X) {
+//                nil : 
+//                 let absurd_rlp_length = RLP.aux.17(List.length(U8,rlp.value))
+//                 Empty.absurd!(absurd_rlp_length(list_u8))
+//                cons : 
+//                  let u8_le_128 = RLP.aux.19(List.length(U8,rlp.value), X.head, X.tail, list_u8)
+//                  replace X with mirror(u8_le_128) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,X.head,List.nil(U8))),RLP.decode.many(List.concat(U8,X.tail,rlp.value))),U8.ltn(X.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
+//                  let u8_le_192 = RLP.aux.20(List.length(U8,rlp.value) X.head, X.tail, list_u8)
+//                  replace X with mirror(u8_le_192) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
+//                  let e3 = RLP.aux.15.sym(X.head, X.tail)
+//     
+//                  ?a-282-
+//              } : RLP.decode(List.concat(U8,X,rlp.value)) == RLP.data(rlp.value)
+//              
+//          } : RLP.decode(X(() List(U8),rlp.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlp.value)),rlp.value))) == RLP.data(rlp.value)
+          //?data
+        node:
+          because_i_said_so!
+//          let ind = RLP.encode_identity(rlps.head.child, ?todo.0)
+//          case Nat.lte(List.length(U8,RLP.encode.many(rlps.head.child)), 55) {
+//            true:
+//              let recover_prefix = ?todo.5 :: Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child))) == U8.to_nat(Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))))
+//              case recover_prefix {
+//                refl:
+//                  let lemma = RLP.aux.split.2(RLP.encode.many(rlps.head.child), RLP.encode.many(rlps.tail), ?todo.2)
+//                  case lemma {
+//                    refl:
+//                      let ind_right = RLP.encode_identity(rlps.tail, ?todo.7)
+//                      let ind_left  = apply(RLP.node, RLP.encode_identity(rlps.head.child, ?todo.8))
+//                      Equal.vapply(2)!!!!(ind_right)!!!(ind_left, List.cons(RLP))
+//                  }: lemma.b(() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))) == _
+//
+//              }: Nat.lte(    recover_prefix.b    ,127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail)))),Nat.lte(    recover_prefix.b    ,191,() List(RLP),RLP.split.length(128,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.concat(U8,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.concat(U8,List.concat(U8,List.nil(U8),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
+//
+//            false:
+//              let recover_prefix = ?todo.1 :: Nat.add(248, List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))) == U8.to_nat(Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))))
+//              case recover_prefix {
+//                refl:
+//                  let lemma = RLP.aux.split.3(RLP.encode.many(rlps.head.child), RLP.encode.many(rlps.tail), ?todo.2, ?todo.3)
+//                  case lemma {
+//                    refl:
+//                      let ind_right = RLP.encode_identity(rlps.tail, ?todo.4)
+//                      let ind_left  = apply(RLP.node, RLP.encode_identity(rlps.head.child, ?todo.5))
+//                      Equal.vapply(2)!!!!(ind_right)!!!(ind_left, List.cons(RLP))
+//
+//                  }: lemma.b( () List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
+//
+//              }: Nat.lte(    recover_prefix.b,    127,() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.nil(U8))),RLP.decode.many(List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail)))),Nat.lte(    recover_prefix.b    ,191,() List(RLP),RLP.split.length(128,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),List.concat(U8,List.concat(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
+//
+//          }: RLP.decode.many(List.concat(U8,List.concat(U8,    self(    () Bytes,List.cons(U8,Nat.to_u8(Nat.add(192,List.length(U8,RLP.encode.many(rlps.head.child)))),List.nil(U8)),List.cons(U8,Nat.to_u8(Nat.add(56,Nat.add(192,List.length(U8,Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))))),Bytes.from_nat(List.length(U8,RLP.encode.many(rlps.head.child))))),RLP.encode.many(rlps.head.child)),RLP.encode.many(rlps.tail))) == List.cons(RLP,RLP.node(rlps.head.child),rlps.tail)
       }!
   }!
 
-//      let remember = Equal.refl(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)))
-//      case Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)) as X
-//            with remember : Equal(Bool, Bool.and(Nat.eql(List.length!(rlp.value),1), U8.ltn(List.head_with_default!(0#8,rlp.value), 128#8)), X)
-//       {
-//        true : 
-//          let break_and1 = RLP.aux.10!!(remember)
-//          let break_and2 = RLP.aux.11!!(remember)
-//          let ensure_non_empty = RLP.aux.12(rlp.value, break_and1)
-//          replace X with mirror(ensure_non_empty) in Maybe.default(RLP,List.head(RLP,X((bytes) List(RLP),List.nil(RLP),(bytes.head) (bytes.tail) U8.ltn(bytes.head,Nat.to_u8(128),() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,bytes.head,List.nil(U8))),RLP.decode.many(bytes.tail)),U8.ltn(bytes.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
-//          replace X with mirror(break_and2) in Maybe.default(RLP,List.head(RLP,X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,List.head_with_default(U8,Nat.to_u8(0),rlp.value),List.nil(U8))),RLP.decode.many(List.nil(U8))),U8.ltn(List.head_with_default(U8,Nat.to_u8(0),rlp.value),Nat.to_u8(192),() List(RLP),RLP.split.length(128,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,rlp.value,() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
-//          let list_length_1 = RlP.new_aux.list_length_1_identity(U8, rlp.value, Nat.to_u8(0), break_and1)
-//          replace X with mirror(list_length_1) in RLP.data(X) == RLP.data(rlp.value)
-//          refl
-//        false : 
-//          let list_u8 = Equal.refl<Bytes, RLP.encode.length(128,List.length(U8,rlp.value))>
-//          case RLP.encode.length(128,List.length(U8,rlp.value)) as X with list_u8 : Equal(Bytes, RLP.encode.length(128,List.length(U8,rlp.value)), X) {
-//            nil : 
-//             let absurd_rlp_length = RLP.aux.17(List.length(U8,rlp.value))
-//             Empty.absurd!(absurd_rlp_length(list_u8))
-//            cons : 
-//              let u8_le_128 = RLP.aux.19(List.length(U8,rlp.value), X.head, X.tail, list_u8)
-//              replace X with mirror(u8_le_128) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),List.cons(RLP,RLP.data(List.cons(U8,X.head,List.nil(U8))),RLP.decode.many(List.concat(U8,X.tail,rlp.value))),U8.ltn(X.head,Nat.to_u8(192),() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail)))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
-//              let u8_le_192 = RLP.aux.20(List.length(U8,rlp.value) X.head, X.tail, list_u8)
-//              replace X with mirror(u8_le_192) in Maybe.default(RLP,List.head(RLP, X(() List(RLP),RLP.split.length(128,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.data(head),RLP.decode.many(tail))),RLP.split.length(192,List.cons(U8,X.head,List.concat(U8,X.tail,rlp.value)),() List(RLP),(head) (tail) List.cons(RLP,RLP.node(RLP.decode.many(head)),RLP.decode.many(tail))))),RLP.data(List.nil(U8))) == RLP.data(rlp.value)
-//              let e3 = RLP.aux.15.sym(X.head, X.tail)
-//
-//              ?a-282-
-//          } : RLP.decode(List.concat(U8,X,rlp.value)) == RLP.data(rlp.value)
-//          
-//      } : RLP.decode(X(() List(U8),rlp.value,List.concat(U8,RLP.encode.length(128,List.length(U8,rlp.value)),rlp.value))) == RLP.data(rlp.value)
 
   // let pf = RLP.encode_identity.go(rlp, [])
   // let e0 = RLP.aux.16(RLP.encode(rlp))