{P : Sort u} →
  {bvExpr : Std.Tactic.BVDecide.BVLogicalExpr} →
    {proveFalse : Lean.Expr → Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr} →
      {unusedHypotheses : Std.HashSet Lean.FVarId} →
        {expr : Lean.Expr} →
          {bvExpr' : Std.Tactic.BVDecide.BVLogicalExpr} →
            {proveFalse' : Lean.Expr → Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr} →
              {unusedHypotheses' : Std.HashSet Lean.FVarId} →
                {expr' : Lean.Expr} →
                  { bvExpr := bvExpr, proveFalse := proveFalse, unusedHypotheses := unusedHypotheses, expr := expr } =
                      { bvExpr := bvExpr', proveFalse := proveFalse', unusedHypotheses := unusedHypotheses',
                        expr := expr' } →
                    (bvExpr = bvExpr' →
                        proveFalse = proveFalse' → unusedHypotheses = unusedHypotheses' → expr = expr' → P) →
                      P