∀ {w : ℕ} (start len : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w) (w_1 start_1 : ℕ)
  (expr_1 : Std.Tactic.BVDecide.BVExpr w_1),
  (Std.Tactic.BVDecide.BVExpr.extract start len expr = Std.Tactic.BVDecide.BVExpr.extract start_1 len expr_1) =
    (w = w_1 ∧ start = start_1 ∧ expr ≍ expr_1)