Theorem: AIG.BinaryRefStream.lhs_getRef_cast (LeanSAT/AIG/RefStream.lean)

State before:
α : 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
Tactic:
simp [cast]
State after:
no goals