∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (n : ℕ),
  Encodable.decodeSum n =
    match n.boddDiv2 with
    | (false, m) => Option.map Sum.inl (Encodable.decode m)
    | (fst, m) => Option.map Sum.inr (Encodable.decode m)