{α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} →
          {motive : Std.Sat.AIG.RefVec.MapTarget aig len → Sort u} →
            ((vec : aig.RefVec len) →
                (func : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α) →
                  [lawful : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref func] →
                    [chainable : Std.Sat.AIG.RefVec.LawfulMapOperator α func] →
                      motive { vec := vec, func := func, lawful := lawful, chainable := chainable }) →
              (t : Std.Sat.AIG.RefVec.MapTarget aig len) → motive t