Theorem: eq_nil_of_subset_nil (Talk/10Aesop.lean)

State before:
α : Type u_1
l : List α
⊢ l ⊆ [] → l = []
Tactic:
aesop (add 1% cases List)
State after:
no goals