(aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
  (w : ℕ) →
    (motive : Std.Tactic.BVDecide.BVExpr.Return aig w → Sort u_1) →
      (x : Std.Tactic.BVDecide.BVExpr.Return aig w) →
        ((aig_1 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
            (lhs : aig_1.RefVec w) →
              (hlaig : aig.decls.size ≤ { aig := aig_1, vec := lhs }.aig.decls.size) →
                (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑⟨{ aig := aig_1, vec := lhs }, hlaig⟩).aig) →
                  motive { result := ⟨{ aig := aig_1, vec := lhs }, hlaig⟩, cache := cache }) →
          motive x