Theorem: AIG.RefStream.getRef_cast (LeanSAT/AIG/RefStream.lean)

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