Theorem: BVExpr.bitblast.FullAdderInput.rhs_cast (LeanSAT/Reflect/BVExpr/BitBlast/Impl/Add.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
s : FullAdderInput aig1
hcast : aig1.decls.size ≤ aig2.decls.size
⊢ (s.cast hcast).rhs = s.rhs.cast hcast
Tactic:
simp [cast]
State after:
no goals