rfl
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ ((choose_indecent_words is_decent a h).get 0).start =
    ∑ j ∈ Finset.range 0, ((choose_indecent_words is_decent a h).get j).length
no goals