Theorem: Array.push_cons_eq_cons_push (Algdata/Data/Array/Basic.lean)

State before:
α : Type u
β : Type v
a b : α
as : Array α
⊢ push (cons a as) b = cons a (push as b)
Tactic:
dsimp [push, cons, List.concat]
State after:
no goals