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