simp [BinaryInput.cast]
α : 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
no goals