cases a
α : Type u_1
inst✝ : BEq α
a b : List α
h : (b == []) = false
⊢ (a ++ b == []) = false
case nil
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
⊢ ([] ++ b == []) = false

case cons
α : Type u_1
inst✝ : BEq α
b : List α
h : (b == []) = false
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝ ++ b == []) = false