{α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} →
          {motive : Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w → Sort u} →
            ((n : ℕ) →
                (lhs : aig.RefVec w) →
                  (rhs : aig.RefVec n) → (pow : ℕ) → motive { n := n, lhs := lhs, rhs := rhs, pow := pow }) →
              (t : Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget aig w) → motive t