rcases (decode e.unpair.1 : Option β) with (_ | b) <;> simp[seq_eq_bind, Option.bind_eq_bind]
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) =
    (decode e.unpair.1).bind fun __do_lift =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1)
case some
β : Type u_1
inst✝ : Encodable β
e : ℕ
this : e.unpair.2 < e + 1
b : β
⊢ Option.map (fun x => b :: x) (decode e.unpair.2) =
    (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun __do_lift => some (b :: __do_lift)