simp [cast]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
aig1 aig2 : AIG α
s : aig1.BinaryRefStream len
idx : Nat
hidx : idx < len
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).lhs.getRef idx hidx = (s.lhs.getRef idx hidx).cast hcast
no goals