Theorem: Qq.List.mem_of_mem (Logic/Vorspiel/Meta.lean)

State before:
α : Type u
a b : α
l : List α
h : a ∈ l
⊢ a ∈ b :: l
Tactic:
simp[h]
State after:
no goals