Theorem: Array.get_push_size (LeanSAT/AIG/Basic.lean)

State before:
α : Type u_1
as : Array α
a : α
⊢ (as.push a)[as.size] = a
Tactic:
simp [Array.get_push]
State after:
no goals