exfalso
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ is_decent (Stream'.take 0 a)
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ False