{α : 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] →
          {motive : Std.Sat.AIG.RefVec.LawfulMapOperator α f → Sort u} →
            (t : Std.Sat.AIG.RefVec.LawfulMapOperator α f) →
              ((chainable :
                    ∀ (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⟧) →
                  motive ⋯) →
                motive t