diff --git a/theories/bitvector.v b/theories/bitvector.v
index f5addf0e41a24825dcd314985467d5498718d8a2..5460c7559675ba330b793ec9bd64957dd4cc451d 100644
--- a/theories/bitvector.v
+++ b/theories/bitvector.v
@@ -4,6 +4,15 @@ From stdpp Require Import options.
 
 Local Open Scope Z_scope.
 
+(* Checks that a term is closed using a trick by Jason Gross. *)
+Ltac check_closed t :=
+  assert_succeeds (
+    let x := fresh "x" in
+    exfalso; pose t as x; revert x;
+    repeat match goal with H : _ |- _ => clear H end;
+    lazymatch goal with H : _ |- _ => fail | _ => idtac end
+  ).
+
 Lemma list_fmap_inj1 {A B} (f1 f2 : A → B) (l : list A) x:
   f1 <$> l = f2 <$> l → x ∈ l → f1 x = f2 x.
 Proof.
@@ -59,7 +68,6 @@ Definition bv_modulus (n : N) : Z := 2 ^ (Z.of_N n).
 Definition bv_half_modulus (n : N) : Z := bv_modulus n `div` 2.
 Definition bv_wrap (n : N) (z : Z) : Z := z `mod` bv_modulus n.
 Definition bv_swrap (n : N) (z : Z) : Z := bv_wrap n (z + bv_half_modulus n) - bv_half_modulus n.
-Local Definition bv_wf (n : N) (z : Z) : Prop := -1 < z < bv_modulus n.
 
 Lemma bv_modulus_pos n :
   0 < bv_modulus n.
@@ -109,12 +117,8 @@ Lemma bv_half_modulus_0:
 Proof. done. Qed.
 
 Lemma bv_half_modulus_twice_mult n:
-  bv_half_modulus n + bv_half_modulus n = (if (decide (n = 0%N)) then 0 else 1) * bv_modulus n.
-Proof. case_decide; subst; [ rewrite bv_half_modulus_0 | rewrite bv_half_modulus_twice]; lia. Qed.
-
-Lemma bv_wf_in_range n z:
-  bv_wf n z ↔ 0 ≤ z < bv_modulus n.
-Proof. unfold bv_wf. lia. Qed.
+  bv_half_modulus n + bv_half_modulus n = (Z.of_N n `min` 1) * bv_modulus n.
+Proof. destruct (decide (n = 0%N)); subst; [ rewrite bv_half_modulus_0 | rewrite bv_half_modulus_twice]; lia. Qed.
 
 Lemma bv_wrap_in_range n z:
   0 ≤ bv_wrap n z < bv_modulus n.
@@ -130,10 +134,6 @@ Proof.
   lia.
 Qed.
 
-Lemma bv_wrap_wf n z :
-  bv_wf n (bv_wrap n z).
-Proof. pose proof (bv_wrap_in_range n z). split; lia. Qed.
-
 Lemma bv_wrap_small n z :
   0 ≤ z < bv_modulus n → bv_wrap n z = z.
 Proof. intros. by apply Z.mod_small. Qed.
@@ -257,20 +257,6 @@ Proof.
   rewrite <-Z.pow_add_r by lia. f_equal. lia.
 Qed.
 
-Lemma bv_wf_bitwise_op {n} op bop n1 n2 :
-  (∀ k, Z.testbit (op n1 n2) k = bop (Z.testbit n1 k) (Z.testbit n2 k)) →
-  (0 ≤ n1 → 0 ≤ n2 → 0 ≤ op n1 n2) →
-  bop false false = false →
-  bv_wf n n1 → bv_wf n n2 → bv_wf n (op n1 n2).
-Proof.
-  intros Hbits Hnonneg Hop [? Hok1]%bv_wf_in_range [? Hok2]%bv_wf_in_range. apply bv_wf_in_range.
-  split; [lia|].
-  apply Z_bounded_iff_bits_nonneg; [lia..|]. intros l ?.
-  eapply Z_bounded_iff_bits_nonneg in Hok1;[|try done; lia..].
-  eapply Z_bounded_iff_bits_nonneg in Hok2;[|try done; lia..].
-  by rewrite Hbits, Hok1, Hok2.
-Qed.
-
 Lemma bv_wrap_land n z :
   bv_wrap n z = Z.land z (Z.ones (Z.of_N n)).
 Proof. by rewrite Z.land_ones by lia. Qed.
@@ -290,13 +276,57 @@ Lemma bv_wrap_spec_high n z i:
   Z.testbit (bv_wrap n z) i = false.
 Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [|done]. lia. Qed.
 
+(** Definition of BvWf *)
+Class BvWf (n : N) (z : Z) : Prop :=
+    bv_wf : (0 <=? z) && (z <? bv_modulus n)
+.
+Global Hint Mode BvWf + + : typeclass_instances.
+Global Instance bv_wf_pi n z : ProofIrrel (BvWf n z).
+Proof. unfold BvWf. apply _. Qed.
+Global Instance bv_wf_dec n z : Decision (BvWf n z).
+Proof. unfold BvWf. apply _. Defined.
+
+Typeclasses Opaque BvWf.
+
+Ltac solve_BvWf :=
+  lazymatch goal with
+    |- BvWf ?n ?v =>
+      check_closed v;
+      try (vm_compute; exact I);
+      fail "Bitvector constant" v "does not fit into" n "bits"
+  end.
+Global Hint Extern 10 (BvWf _ _) => solve_BvWf : typeclass_instances.
+
+Lemma bv_wf_in_range n z:
+  BvWf n z ↔ 0 ≤ z < bv_modulus n.
+Proof. unfold BvWf. by rewrite andb_True, !Is_true_true, Z.leb_le, Z.ltb_lt. Qed.
+
+Lemma bv_wrap_wf n z :
+  BvWf n (bv_wrap n z).
+Proof. apply bv_wf_in_range. apply bv_wrap_in_range. Qed.
+
+Lemma bv_wf_bitwise_op {n} op bop n1 n2 :
+  (∀ k, Z.testbit (op n1 n2) k = bop (Z.testbit n1 k) (Z.testbit n2 k)) →
+  (0 ≤ n1 → 0 ≤ n2 → 0 ≤ op n1 n2) →
+  bop false false = false →
+  BvWf n n1 → BvWf n n2 → BvWf n (op n1 n2).
+Proof.
+  intros Hbits Hnonneg Hop [? Hok1]%bv_wf_in_range [? Hok2]%bv_wf_in_range. apply bv_wf_in_range.
+  split; [lia|].
+  apply Z_bounded_iff_bits_nonneg; [lia..|]. intros l ?.
+  eapply Z_bounded_iff_bits_nonneg in Hok1;[|try done; lia..].
+  eapply Z_bounded_iff_bits_nonneg in Hok2;[|try done; lia..].
+  by rewrite Hbits, Hok1, Hok2.
+Qed.
+
 (** * Definition of [bv n] *)
 Record bv (n : N) := BV {
   bv_unsigned : Z;
-  bv_is_wf : bv_wf n bv_unsigned;
+  bv_is_wf : BvWf n bv_unsigned;
 }.
 Global Arguments bv_unsigned {_}.
 Global Arguments bv_is_wf {_}.
+Global Arguments BV _ _ {_}.
 Add Printing Constructor bv.
 
 Global Arguments bv_unsigned : simpl never.
@@ -315,10 +345,10 @@ Lemma bv_neq n (b1 b2 : bv n) :
 Proof. unfold not. by rewrite bv_eq. Qed.
 
 Definition Z_to_bv_checked (n : N) (z : Z) : option (bv n) :=
-  guard (bv_wf n z) as H; Some (BV n z H).
+  guard (BvWf n z) as H; Some (@BV n z H).
 
 Program Definition Z_to_bv (n : N) (z : Z) : bv n :=
-  BV n (bv_wrap n z) _.
+  @BV n (bv_wrap n z) _.
 Next Obligation. apply bv_wrap_wf. Qed.
 
 Lemma Z_to_bv_unsigned n z:
@@ -335,11 +365,11 @@ Lemma Z_to_bv_small n z:
 Proof. rewrite Z_to_bv_unsigned. apply bv_wrap_small. Qed.
 
 Lemma bv_unsigned_BV n z Hwf:
-  bv_unsigned (BV n z Hwf) = z.
+  bv_unsigned (@BV n z Hwf) = z.
 Proof. done. Qed.
 
 Lemma bv_signed_BV n z Hwf:
-  bv_signed (BV n z Hwf) = bv_swrap n z.
+  bv_signed (@BV n z Hwf) = bv_swrap n z.
 Proof. done. Qed.
 
 Lemma bv_unsigned_in_range n (b : bv n):
@@ -421,7 +451,7 @@ Proof.
 Qed.
 
 
-Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(BV _ v1 p1) '(BV _ v2 p2),
+Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(@BV _ v1 p1) '(@BV _ v2 p2),
    match decide (v1 = v2) with
    | left eqv => left _
    | right eqv => right _
@@ -448,30 +478,14 @@ Next Obligation.
   - apply lookup_seqZ. split; [done|]. rewrite Z2Nat.id; lia.
   - apply bv_eq. rewrite Z_to_bv_small; rewrite Z2Nat.id; lia.
 Qed.
-
 Lemma bv_1_ind (P : bv 1 → Prop) :
-  P (BV 1 1 ltac:(done)) → P (BV 1 0 ltac:(done)) → ∀ b : bv 1, P b.
+  P (@BV 1 1 I) → P (@BV 1 0 I) → ∀ b : bv 1, P b.
 Proof.
   intros ??. apply Forall_finite. repeat constructor.
-  - by assert ((BV 1 0 (conj eq_refl eq_refl)) = (Z_to_bv 1 (Z.of_nat 0 + 0))) as <- by by apply bv_eq.
-  - by assert ((BV 1 1 (conj eq_refl eq_refl)) = (Z_to_bv 1 (Z.of_nat 1 + 0))) as <- by by apply bv_eq.
+  - by assert ((@BV 1 0 I) = (Z_to_bv 1 (Z.of_nat 0 + 0))) as <- by by apply bv_eq.
+  - by assert ((@BV 1 1 I) = (Z_to_bv 1 (Z.of_nat 1 + 0))) as <- by by apply bv_eq.
 Qed.
 
-
-
-(** * Notation for [bv n] *)
-Ltac solve_bitvector_eq :=
-  try (vm_compute; exact (conj eq_refl eq_refl));
-  lazymatch goal with
-    |- bv_wf ?n ?v =>
-    fail "Bitvector constant" v "does not fit into" n "bits"
-  end.
-
-Notation "'[BV{' l }  v ]" := (BV l v _) (at level 9, only printing) : stdpp_scope.
-(* TODO: Somehow the following version creates a warning. *)
-(* Notation "'[BV{' l } v ]" := (BV l v _) (at level 9, format "[BV{ l }  v ]", only printing) : stdpp_scope. *)
-Notation "'[BV{' l }  v ]" := (BV l v ltac:(solve_bitvector_eq)) (at level 9, only parsing) : stdpp_scope.
-
 (** * Automation *)
 Ltac bv_saturate :=
   repeat match goal with b : bv _ |- _ => first [
@@ -568,107 +582,9 @@ Ltac bv_wrap_simplify :=
 Ltac bv_wrap_simplify_solve :=
   bv_wrap_simplify; f_equal; lia.
 
-(** ** ring_simplify-based automation for simplifying bv_wrap *)
-(* TODO: Where to put the following automation? And how should it best be implemented? *)
-Definition bv_wrap_simplify_marker (z1 z2 : Z) : Z := z1 + z2.
-
-Lemma bv_wrap_simplify_marker_intro n z x:
-  bv_wrap n (bv_wrap_simplify_marker z 0) = x →
-  bv_wrap n z = x.
-Proof. intros <-. unfold bv_wrap_simplify_marker. f_equal. lia. Qed.
-
-Lemma bv_wrap_simplify_marker_move n z1 z2 x m:
-  bv_wrap n (bv_wrap_simplify_marker z1 (z2 + m)) = x →
-  bv_wrap n (bv_wrap_simplify_marker (z1 + z2) m) = x.
-Proof. intros <-. unfold bv_wrap_simplify_marker. f_equal. lia. Qed.
-
-Lemma bv_wrap_simplify_marker_remove n z1 z2 x m:
-  bv_wrap n (bv_wrap_simplify_marker z1 m) = x →
-  bv_wrap n (bv_wrap_simplify_marker (z1 + z2 * bv_modulus n) m) = x.
-Proof.
-  intros <-. unfold bv_wrap_simplify_marker.
-  assert ((z1 + z2 * bv_modulus n + m) = (z1 + m + z2 * bv_modulus n)) as -> by lia.
-  by apply bv_wrap_add_modulus.
-Qed.
-
-Lemma bv_wrap_simplify_marker_remove_sub n z1 z2 x m:
-  bv_wrap n (bv_wrap_simplify_marker z1 m) = x →
-  bv_wrap n (bv_wrap_simplify_marker (z1 - z2 * bv_modulus n) m) = x.
-Proof.
-  intros <-. unfold bv_wrap_simplify_marker.
-  assert ((z1 - z2 * bv_modulus n + m) = (z1 + m - z2 * bv_modulus n)) as -> by lia.
-  by apply bv_wrap_sub_modulus.
-Qed.
-
-Lemma bv_wrap_simplify_marker_move_end n z x m:
-  bv_wrap n (z + m) = x →
-  bv_wrap n (bv_wrap_simplify_marker z m) = x.
-Proof. intros <-. unfold bv_wrap_simplify_marker. f_equal. Qed.
-
-Lemma bv_wrap_simplify_marker_remove_end n z x m:
-  bv_wrap n m = x →
-  bv_wrap n (bv_wrap_simplify_marker (z * bv_modulus n) m) = x.
-Proof. intros <-. unfold bv_wrap_simplify_marker. rewrite Z.add_comm. apply bv_wrap_add_modulus. Qed.
-
-Lemma bv_wrap_simplify_marker_remove_end_opp n z x m:
-  bv_wrap n m = x →
-  bv_wrap n (bv_wrap_simplify_marker (- z * bv_modulus n) m) = x.
-Proof. intros <-. unfold bv_wrap_simplify_marker. rewrite Z.add_comm. apply bv_wrap_add_modulus. Qed.
-
-Lemma Zmul_assoc_comm n2 n1 n3 : n1 * n2 * n3 = n1 * n3 * n2.
-Proof. lia. Qed.
-
-Lemma Zpow_2_mul a : a ^ 2 = a * a.
-Proof. lia. Qed.
-
-Local Ltac bv_wrap_simplify_cancel :=
-  apply bv_wrap_simplify_marker_intro;
-  repeat first [ apply bv_wrap_simplify_marker_remove | apply bv_wrap_simplify_marker_remove_sub | apply bv_wrap_simplify_marker_move];
-  first [ apply bv_wrap_simplify_marker_remove_end | apply bv_wrap_simplify_marker_remove_end_opp | apply bv_wrap_simplify_marker_move_end].
-
-(** [bv_wrap_simplify_left] applies for goals of the form [bv_wrap n z1 = _] and
- tries to simplify them by removing any [bv_wrap] inside z1. *)
-Ltac bv_wrap_simplify_left' :=
-  repeat lazymatch goal with
-         | |- bv_wrap _ ?x = _ =>
-             match x with
-             | context [ bv_wrap ?n ?z ] =>
-                 let x := fresh "x" in
-                 let Heq := fresh "Heq" in
-                 pose proof (bv_wrap_factor_intro n z) as [x [_ Heq]];
-                 rewrite !Heq;
-                 clear Heq
-             end
-         end;
-  match goal with | |- bv_wrap _ ?z = _ => ring_simplify z end;
-  repeat match goal with | |- context [- bv_modulus ?n * ?z] => rewrite (Z.mul_opp_comm (bv_modulus n) z) end;
-  repeat match goal with | |- context [bv_modulus ?n * ?z] => rewrite (Z.mul_comm (bv_modulus n) z) end;
-  repeat match goal with | |- context [(bv_modulus ?n ^ ?m) * ?z] => rewrite (Z.mul_comm (bv_modulus n ^ m) z) end;
-  repeat match goal with | |- context [?z1 * bv_modulus ?n * ?z2] => rewrite (Zmul_assoc_comm (bv_modulus n) z1 z2) end;
-  repeat match goal with | |- context [?z1 * (bv_modulus ?n ^ ?m) * ?z2] => rewrite (Zmul_assoc_comm (bv_modulus n ^ m) z1 z2) end;
-  repeat match goal with | |- context [?n ^ 2] => rewrite (Zpow_2_mul n) end;
-  repeat match goal with | |- context [?z1 * (?z2 * ?z3)] => rewrite (Z.mul_assoc z1 z2 z3) end;
-
-  bv_wrap_simplify_cancel;
-  match goal with | |- bv_wrap _ ?z = _ => ring_simplify z end.
-
-(** [bv_wrap_simplify] applies for goals of the form [bv_wrap n z1 = bv_wrap n z2] and
-[bv_swrap n z1 = bv_swrap n z2] and tries to simplify them by removing any [bv_wrap]
-and [bv_swrap] inside z1 and z2. *)
-Ltac bv_wrap_simplify' :=
-  unfold bv_signed, bv_swrap;
-  try match goal with | |- _ - _ = _ - _ => f_equal end;
-  bv_wrap_simplify_left;
-  symmetry;
-  bv_wrap_simplify_left;
-  symmetry.
-
-Ltac bv_wrap_simplify_solve' :=
-  bv_wrap_simplify; f_equal; lia.
-
 (** * Operations on [bv n] *)
 Program Definition bv_0 (n : N) :=
-  BV n 0 _.
+  @BV n 0 _.
 Next Obligation.
   intros n. apply bv_wf_in_range. split; [done| apply bv_modulus_pos].
 Qed.
@@ -689,7 +605,7 @@ Definition bv_opp {n} (x : bv n) : bv n := (* SMT: bvneg *)
 Definition bv_mul {n} (x y : bv n) : bv n := (* SMT: bvmul *)
   Z_to_bv n (Z.mul (bv_unsigned x) (bv_unsigned y)).
 Program Definition bv_divu {n} (x y : bv n) : bv n := (* SMT: bvudiv *)
-  BV n (Z.div (bv_unsigned x) (bv_unsigned y)) _.
+  @BV n (Z.div (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
   intros n x y. apply bv_wf_in_range. bv_saturate.
   destruct (decide (bv_unsigned y = 0)) as [->|?].
@@ -699,7 +615,7 @@ Next Obligation.
   apply Z.div_le_upper_bound; [ lia|]. nia.
 Qed.
 Program Definition bv_modu {n} (x y : bv n) : bv n := (* SMT: bvurem *)
-  BV n (Z.modulo (bv_unsigned x) (bv_unsigned y)) _.
+  @BV n (Z.modulo (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
   intros n x y. apply bv_wf_in_range. bv_saturate.
   destruct (decide (bv_unsigned y = 0)) as [->|?].
@@ -720,7 +636,7 @@ Definition bv_rems {n} (x y : bv n) : bv n := (* SMT: bvsrem *)
 Definition bv_shiftl {n} (x y : bv n) : bv n := (* SMT: bvshl *)
   Z_to_bv n (Z.shiftl (bv_unsigned x) (bv_unsigned y)).
 Program Definition bv_shiftr {n} (x y : bv n) : bv n := (* SMT: bvlshr *)
-  BV n (Z.shiftr (bv_unsigned x) (bv_unsigned y)) _.
+  @BV n (Z.shiftr (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
   intros n x y. apply bv_wf_in_range. bv_saturate.
   split; [ apply Z.shiftr_nonneg; lia|].
@@ -733,17 +649,17 @@ Definition bv_ashiftr {n} (x y : bv n) : bv n := (* SMT: bvashr *)
   Z_to_bv n (Z.shiftr (bv_signed x) (bv_unsigned y)).
 
 Program Definition bv_or {n} (x y : bv n) : bv n := (* SMT: bvor *)
-  BV n (Z.lor (bv_unsigned x) (bv_unsigned y)) _.
+  @BV n (Z.lor (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
   intros. eapply bv_wf_bitwise_op; [ apply Z.lor_spec | by intros; eapply Z.lor_nonneg | done | apply bv_is_wf..].
 Qed.
 Program Definition bv_and {n} (x y : bv n) : bv n := (* SMT: bvand *)
-  BV n (Z.land (bv_unsigned x) (bv_unsigned y)) _.
+  @BV n (Z.land (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
   intros. eapply bv_wf_bitwise_op; [ apply Z.land_spec | intros; eapply Z.land_nonneg; by left | done | apply bv_is_wf..].
 Qed.
 Program Definition bv_xor {n} (x y : bv n) : bv n := (* SMT: bvxor *)
-  BV n (Z.lxor (bv_unsigned x) (bv_unsigned y)) _.
+  @BV n (Z.lxor (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
   intros. eapply bv_wf_bitwise_op; [ apply Z.lxor_spec | intros; eapply Z.lxor_nonneg; naive_solver | done | apply bv_is_wf..].
 Qed.
@@ -1337,13 +1253,7 @@ Lemma bvn_eq (b1 b2 : bvn) :
 Proof. split; [ naive_solver|]. destruct b1, b2; simpl; intros [??]. subst. f_equal. by apply bv_eq. Qed.
 
 Global Program Instance bvn_eq_dec : EqDecision bvn := λ '(@bv_to_bvn n1 b1) '(@bv_to_bvn n2 b2),
-   match decide (n1 = n2) with
-   | left eqv => match decide (bv_unsigned b1 = bv_unsigned b2) with
-                | left eqb => left _
-                | right eqb => right _
-                end
-   | right eqv => right _
-   end.
+   cast_if_and (decide (n1 = n2)) (decide (bv_unsigned b1 = bv_unsigned b2)).
 (* TODO: The following does not compute to eq_refl*)
 Next Obligation. intros. apply bvn_eq. naive_solver. Qed.
 Next Obligation. intros. intros ?%bvn_eq. naive_solver. Qed.
@@ -1360,9 +1270,9 @@ Global Coercion bv_to_bvn : bv >-> bvn.
 
 (** * tests *)
 Section test.
-Goal ([BV{10} 3 ] = [BV{10} 5]). Abort.
-Fail Goal ([BV{2} 3 ] = [BV{10} 5]).
-Goal ([BV{2} 3 ] =@{bvn} [BV{10} 5]). Abort.
-Fail Goal ([BV{2} 4 ] = [BV{2} 5]).
-Goal bvn_to_bv 2 [BV{2} 3] = Some [BV{2} 3]. done. Abort.
+Goal (BV 10 3 = BV 10 5). Abort.
+Fail Goal (BV 2 3 = BV 10 5).
+Goal (BV 2 3 =@{bvn} BV 10 5). Abort.
+Fail Goal (BV 2 4 = BV 2 5).
+Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). done. Abort.
 End test.