Theorem: Array.mem_of_push (RegexCorrectness/Data/Array.lean)

State before:
α : Type u_1
a : Array α
x : α
⊢ x ∈ a.push x
Tactic:
simp [Array.mem_def]
State after:
no goals