Theorem: list_app_cons_ne_nil (Katydid/Std/Lists.lean)

State before:
α : Type u_1
y : α
xs ys : List α
⊢ xs ++ y :: ys ≠ []
Tactic:
cases xs <;> { intro h' ; contradiction }
State after:
no goals

State before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ y :: ys ≠ []
Tactic:
intro h'
State after:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : head✝ :: tail✝ ++ y :: ys = []
⊢ False

State before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : head✝ :: tail✝ ++ y :: ys = []
⊢ False
Tactic:
contradiction
State after:
no goals