rwa [Stream'.get_inits] at ht
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n + 1
ht : is_decent (a.inits.get n)
⊢ is_decent (Stream'.take (n + 1) a)
no goals