∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α]
  {f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α}
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f],
  (∀ (aig : Std.Sat.AIG α) (input1 input2 : aig.Ref) (h : aig.decls.size ≤ (f aig input1).aig.decls.size)
      (assign : α → Bool), ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧) →
    Std.Sat.AIG.RefVec.LawfulMapOperator α f