simp[all_prefixes, Stream'.all_def] at h
α : Type
is_decent : List α → Prop
a : Stream' α
h : ¬all_prefixes is_decent a
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∃ x, ¬is_decent (Stream'.take (x + 1) a)
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)