Theorem: AIG.RefStream.LawfulMapOperator.denote_prefix_cast_ref (LeanSAT/AIG/RefStreamOperator.lean)

State before:
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
assign : α → Bool
aig : AIG α
input1 input2 : aig.Ref
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
h : aig.decls.size ≤ (f aig input1).aig.decls.size
⊢ ⟦f (f aig input1).aig (input2.cast h), assign⟧ = ⟦f aig input2, assign⟧
Tactic:
rw [LawfulMapOperator.chainable]
State after:
no goals