Theorem: AIG.LawfulOperator.denote_cast_entry (LeanSAT/AIG/LawfulOperator.lean)

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ ⟦{ aig := (f entry.aig input).aig, ref := entry.ref.cast h }, assign⟧ = ⟦entry, assign⟧
Tactic:
simp [Ref.cast]
State after:
no goals