diff --git a/theories/bitvector.v b/theories/bitvector.v
index 798d2111a4855594c3c9b48d976629f56c2391e2..b78dde31dbd38817f50301aec661fadee4b5d812 100644
--- a/theories/bitvector.v
+++ b/theories/bitvector.v
@@ -4,40 +4,6 @@ From stdpp Require Import options.
 
 Local Open Scope Z_scope.
 
-Lemma Z_bounded_iff_bits_nonneg k n :
-  0 ≤ k → 0 ≤ n →
-  n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
-Proof.
-  intros.
-  destruct (decide (n = 0)) as [->|].
-  - setoid_rewrite Z.bits_0. split; [done|]. intros. by apply Z.pow_pos_nonneg.
-  - split.
-    + intros Hb%Z.log2_lt_pow2 l Hl; [| lia]. apply Z.bits_above_log2; lia.
-    + intros Hl.
-      destruct (decide (n < 2^k)); [done|].
-      assert (Z.testbit n (Z.log2 n) = false) as Hbit.
-      { apply Hl, Z.log2_le_pow2; lia. }
-      rewrite Z.bit_log2 in Hbit; [done| lia].
-Qed.
-
-Lemma Z_bounded_iff_bits_nonneg' k n :
-  0 ≤ k → 0 ≤ n →
-  0 ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
-Proof.
-  intros ??. split.
-  - intros ?. apply Z_bounded_iff_bits_nonneg; lia.
-  - intros ?%Z_bounded_iff_bits_nonneg; lia.
-Qed.
-
-Tactic Notation "learn_hyp" constr(p) "as" ident(H') :=
-  let P := type of p in
-  match goal with
-  | H : P |- _ => fail 1
-  | _ => pose proof p as H'
-  end.
-Tactic Notation "learn_hyp" constr(p) :=
-  let H := fresh in learn_hyp p as H.
-
 Lemma Zmul_assoc_comm n2 n1 n3 : n1 * n2 * n3 = n1 * n3 * n2.
 Proof. lia. Qed.
 
@@ -100,13 +66,13 @@ Proof.
     rewrite !Z_ones_spec by nia. repeat case_decide; try done; nia.
 Qed.
 
-Lemma Z_to_little_bound x m n z:
+Lemma Z_to_little_bound m n z:
   0 ≤ n →
-  x ∈ Z_to_little m n z → 0 ≤ x < 2 ^ n.
+  Forall (λ b, 0 ≤ b < 2 ^ n) (Z_to_little m n z).
 Proof.
-  intros ?. revert z. induction m as [|m IH]; simpl. { by intros ? ?%elem_of_nil. }
-  intros ?. intros [->|?%IH]%elem_of_cons; [|done].
-  rewrite Z.land_ones by lia.
+  intros ?. revert z. induction m as [|m IH]; simpl.
+  { by constructor. }
+  intros ?. constructor; [|by apply IH]. rewrite Z.land_ones by lia.
   apply Z.mod_pos_bound. apply Z.pow_pos_nonneg; lia.
 Qed.
 
@@ -135,7 +101,7 @@ 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.
-Definition bv_ok (n : N) (z : Z) : Prop := -1 < z < bv_modulus n.
+Definition bv_wf (n : N) (z : Z) : Prop := -1 < z < bv_modulus n.
 
 Lemma bv_modulus_pos n :
   0 < bv_modulus n.
@@ -162,12 +128,12 @@ 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_ok_in_range n z:
-  bv_ok n z ↔ 0 ≤ z < bv_modulus n.
-Proof. unfold bv_ok. lia. Qed.
+Lemma bv_wf_in_range n z:
+  bv_wf n z ↔ 0 ≤ z < bv_modulus n.
+Proof. unfold bv_wf. lia. Qed.
 
-Lemma bv_wrap_ok n z :
-  bv_ok n (bv_wrap n z).
+Lemma bv_wrap_wf n z :
+  bv_wf n (bv_wrap n z).
 Proof.
   unfold bv_wrap.
   pose proof (Z.mod_pos_bound z (bv_modulus n)) as [??]. { apply bv_modulus_pos. }
@@ -226,13 +192,13 @@ Lemma bv_swrap_wrap n z:
   bv_swrap n (bv_wrap n z) = bv_swrap n z.
 Proof. unfold bv_swrap, bv_wrap. by rewrite Zplus_mod_idemp_l. Qed.
 
-Lemma bv_ok_bitwise_op {n} op bop n1 n2 :
+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_ok n n1 → bv_ok n n2 → bv_ok n (op n1 n2).
+  bv_wf n n1 → bv_wf n n2 → bv_wf n (op n1 n2).
 Proof.
-  intros Hbits Hnonneg Hop [? Hok1]%bv_ok_in_range [? Hok2]%bv_ok_in_range. apply bv_ok_in_range.
+  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..].
@@ -243,10 +209,10 @@ Qed.
 (** * Definition of [bv n] *)
 Record bv (n : N) := BV {
   bv_unsigned : Z;
-  bv_is_ok : bv_ok n bv_unsigned;
+  bv_is_wf : bv_wf n bv_unsigned;
 }.
 Global Arguments bv_unsigned {_}.
-Global Arguments bv_is_ok {_}.
+Global Arguments bv_is_wf {_}.
 
 Definition bv_signed {n} (b : bv n) := bv_swrap n (bv_unsigned b).
 
@@ -268,20 +234,20 @@ Next Obligation. intros. by injection. Qed.
 Global Instance bv_countable n : Countable (bv n).
 Proof.
   refine (inj_countable bv_unsigned
-    (λ x, match decide (bv_ok n x) with | left b => Some (BV n x b) | _ => None end) _).
+    (λ x, match decide (bv_wf n x) with | left b => Some (BV n x b) | _ => None end) _).
   intros x. case_decide; [ f_equal; by apply bv_eq|].
-  by pose proof bv_is_ok x.
+  by pose proof bv_is_wf x.
 Qed.
 
 Definition bv_of_Z_checked (n : N) (z : Z) : option (bv n) :=
-  match decide (bv_ok n z) with
+  match decide (bv_wf n z) with
   | left Heq => Some (BV n z Heq)
   | right _ => None
   end.
 
 Program Definition bv_of_Z (n : N) (z : Z) : bv n :=
   BV n (bv_wrap n z) _.
-Next Obligation. apply bv_wrap_ok. Qed.
+Next Obligation. apply bv_wrap_wf. Qed.
 
 Lemma bv_of_Z_unsigned n z:
   bv_unsigned (bv_of_Z n z) = bv_wrap n z.
@@ -301,7 +267,7 @@ Proof. rewrite bv_of_Z_unsigned. apply bv_wrap_small. Qed.
 
 Lemma bv_in_range n (b : bv n):
   0 ≤ bv_unsigned b < bv_modulus n.
-Proof. apply bv_ok_in_range. apply bv_is_ok. Qed.
+Proof. apply bv_wf_in_range. apply bv_is_wf. Qed.
 
 Global Program Instance bv_finite n : Finite (bv n) :=
   {| enum := bv_of_Z n <$> (seqZ 0 (bv_modulus n)) |}.
@@ -426,7 +392,7 @@ Ltac bv_wrap_simplify_solve :=
 Program Definition bv_0 (n : N) :=
   BV n 0 _.
 Next Obligation.
-  intros n. apply bv_ok_in_range. split; [done| apply bv_modulus_pos].
+  intros n. apply bv_wf_in_range. split; [done| apply bv_modulus_pos].
 Qed.
 
 Definition bv_succ {n} (x : bv n) : bv n :=
@@ -446,7 +412,7 @@ Definition bv_mul {n} (x y : bv n) : bv n := (* SMT: bvmul *)
 Program Definition bv_divu {n} (x y : bv n) : bv n := (* SMT: bvudiv *)
   BV n (Z.div (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
-  intros n x y. apply bv_ok_in_range. bv_saturate.
+  intros n x y. apply bv_wf_in_range. bv_saturate.
   destruct (decide (bv_unsigned y = 0)) as [->|?].
   { rewrite Zdiv_0_r. lia. }
   split; [ apply Z.div_pos; lia |].
@@ -456,7 +422,7 @@ Qed.
 Program Definition bv_modu {n} (x y : bv n) : bv n := (* SMT: bvurem *)
   BV n (Z.modulo (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
-  intros n x y. apply bv_ok_in_range. bv_saturate.
+  intros n x y. apply bv_wf_in_range. bv_saturate.
   destruct (decide (bv_unsigned y = 0)) as [->|?].
   { rewrite Zmod_0_r. lia. }
   split; [ apply Z_mod_pos; lia |].
@@ -477,7 +443,7 @@ Definition bv_shiftl {n} (x y : bv n) : bv n := (* SMT: bvshl *)
 Program Definition bv_shiftr {n} (x y : bv n) : bv n := (* SMT: bvlshr *)
   BV n (Z.shiftr (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
-  intros n x y. apply bv_ok_in_range. bv_saturate.
+  intros n x y. apply bv_wf_in_range. bv_saturate.
   split; [ apply Z.shiftr_nonneg; lia|].
   rewrite Z.shiftr_div_pow2; [|lia].
   apply (Z.le_lt_trans _ (bv_unsigned x)); [|lia].
@@ -490,17 +456,17 @@ Definition bv_ashiftr {n} (x y : bv n) : bv n := (* SMT: bvashr *)
 Program Definition bv_or {n} (x y : bv n) : bv n := (* SMT: bvor *)
   BV n (Z.lor (bv_unsigned x) (bv_unsigned y)) _.
 Next Obligation.
-  intros. eapply bv_ok_bitwise_op; [ apply Z.lor_spec | by intros; eapply Z.lor_nonneg | done | apply bv_is_ok..].
+  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)) _.
 Next Obligation.
-  intros. eapply bv_ok_bitwise_op; [ apply Z.land_spec | intros; eapply Z.land_nonneg; by left | done | apply bv_is_ok..].
+  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)) _.
 Next Obligation.
-  intros. eapply bv_ok_bitwise_op; [ apply Z.lxor_spec | intros; eapply Z.lxor_nonneg; naive_solver | done | apply bv_is_ok..].
+  intros. eapply bv_wf_bitwise_op; [ apply Z.lxor_spec | intros; eapply Z.lxor_nonneg; naive_solver | done | apply bv_is_wf..].
 Qed.
 Program Definition bv_not {n} (x : bv n) : bv n := (* SMT: bvnot *)
   bv_of_Z n (Z.lnot (bv_unsigned x)).
@@ -508,7 +474,7 @@ Program Definition bv_not {n} (x : bv n) : bv n := (* SMT: bvnot *)
 Program Definition bv_zero_extend {n} (z : N) (b : bv n) : bv (n + z) := (* SMT: zero_extend *)
   BV _ (bv_unsigned b) _.
 Next Obligation.
-  intros. apply bv_ok_in_range. rewrite bv_modulus_add. bv_saturate.
+  intros. apply bv_wf_in_range. rewrite bv_modulus_add. bv_saturate.
   pose proof (bv_modulus_pos z). nia.
 Qed.
 
@@ -524,7 +490,7 @@ Program Definition bv_extract {n} (s l : N) (b : bv n) : bv l :=
   BV l (Z.land (bv_unsigned b ≫ Z.of_N s) (Z.ones (Z.of_N l))) _.
 Next Obligation.
   intros.
-  apply bv_ok_in_range.
+  apply bv_wf_in_range.
   apply Z_bounded_iff_bits_nonneg'; [lia | |].
   { apply Z.land_nonneg. left. apply Z.shiftr_nonneg. bv_saturate. lia. }
   intros k ?. rewrite Z.land_spec. apply andb_false_intro2.
@@ -535,7 +501,7 @@ Program Definition bv_concat {n1 n2} (b1 : bv n1) (b2 : bv n2) : bv (n1 + n2) :=
   BV _ (Z.lor (bv_unsigned b1 ≪ Z.of_N n2) (bv_unsigned b2)) _.
 Next Obligation.
   intros.
-  apply bv_ok_in_range.
+  apply bv_wf_in_range.
   apply Z_bounded_iff_bits_nonneg'; [lia | |].
   { apply Z.lor_nonneg. bv_saturate. split; [|lia]. apply Z.shiftl_nonneg. lia. }
   intros k ?. rewrite Z.lor_spec, Z.shiftl_spec; [|lia].
@@ -609,7 +575,8 @@ Section little.
     rewrite list_lookup_fmap, list_lookup_fmap.
     destruct (Z_to_little m (Z.of_N n) z !! i) eqn: Heq; [simpl |done].
     rewrite bv_of_Z_small; [done|].
-    eapply Z_to_little_bound; [lia|]. by eapply elem_of_list_lookup_2.
+    eapply (Forall_forall (λ z, _ ≤ z < _)); [ eapply Z_to_little_bound; lia | ].
+    by eapply elem_of_list_lookup_2.
   Qed.
 
   Lemma bv_to_of_little m n bs: