Theorem: AIG.BinaryInput.cast_each (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
lhs rhs : aig1.Ref
h1 h2 : aig1.decls.size ≤ aig2.decls.size
⊢ { lhs := lhs.cast h1, rhs := rhs.cast h2 } = { lhs := lhs, rhs := rhs }.cast h2
Tactic:
simp [BinaryInput.cast]
State after:
no goals