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

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