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

State before:
α : Type u_1
x : α
xs : List α
⊢ [x] ++ xs ≠ []
Tactic:
intro h'
State after:
α : Type u_1
x : α
xs : List α
h' : [x] ++ xs = []
⊢ False

State before:
α : Type u_1
x : α
xs : List α
h' : [x] ++ xs = []
⊢ False
Tactic:
contradiction
State after:
no goals