{α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : aig.ExtendTarget newWidth → Sort u_1) →
            (target : aig.ExtendTarget newWidth) →
              ((width : ℕ) → (input : aig.RefVec width) → motive { w := width, vec := input }) → motive target