have := s.hlen
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
⊢ (s.pushRef ref).getRef len ⋯ = ref
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
this : s.refs.size = len
⊢ (s.pushRef ref).getRef len ⋯ = ref