∀ {α : Type u_1} [inst : Encodable α] (x : ℕ),
  Encodable.decodeList x =
    match x with
    | 0 => some []
    | v.succ =>
      match Nat.unpair v, ⋯ with
      | (v₁, v₂), h =>
        have this := ⋯;
        (fun x1 x2 => x1 :: x2) <$> Encodable.decode v₁ <*> Encodable.decodeList v₂