∀ {w : ℕ} (ll lr : ℕ) (llhs : Std.Tactic.BVDecide.BVExpr ll) (lrhs : Std.Tactic.BVDecide.BVExpr lr) (lh : w = ll + lr)
  (lhs : Std.Tactic.BVDecide.BVExpr w) (op : Std.Tactic.BVDecide.BVBinOp) (rhs : Std.Tactic.BVDecide.BVExpr w),
  ¬llhs.append lrhs lh = lhs.bin op rhs