theorem
Array.of_push_eq_push
{α : Type u_1}
{a : α}
{b : α}
{as : Array α}
{bs : Array α}
(h : Array.push as a = Array.push bs b)
:
@[simp]
theorem
List.toArray_eq_toArray_eq
{α : Type u_1}
(as : List α)
(bs : List α)
:
(List.toArray as = List.toArray bs) = (as = bs)