Removed deprecated features

15 files changed, 499 insertions, 499 deletions

diff --git a/src/Misc.v b/src/Misc.v
index 0317bda..86dc1aa 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -25,7 +25,7 @@ Proof. intros [ | ]; reflexivity. Qed.
 
 (** Lemmas about Int63 *)
 
-Lemma reflect_eqb : forall i j, reflect (i = j)%Z (i == j).
+Lemma reflect_eqb : forall i j, reflect (i = j)%Z (i =? j).
 Proof.
  intros; apply iff_reflect.
  symmetry;apply eqb_spec.
@@ -43,7 +43,7 @@ Proof.
 Qed.
 
 Lemma le_eq : forall i j,
-  (j <= i) = true -> (j + 1 <= i) = false -> i = j.
+  (j <=? i) = true -> (j + 1 <=? i) = false -> i = j.
 Proof.
   intros i j; rewrite leb_spec; destruct (dec_Zle [|j+1|] [|i|]) as [H|H].
   rewrite <- leb_spec in H; rewrite H; discriminate.
@@ -59,18 +59,18 @@ Proof.
   rewrite H2, Z_mod_same_full in H; elim H; destruct (to_Z_bounded i) as [H3 _]; assumption.
 Qed.
 
-Lemma leb_0 : forall x, 0 <= x = true.
+Lemma leb_0 : forall x, 0 <=? x = true.
 Proof.
  intros x;rewrite leb_spec;destruct (to_Z_bounded x);trivial.
 Qed.
 
-Lemma leb_refl : forall n, n <= n = true.
+Lemma leb_refl : forall n, n <=? n = true.
 Proof.
  intros n;rewrite leb_spec;apply Z.le_refl.
 Qed.
 
 Lemma lt_eq : forall i j,
-  (i < j + 1) = true -> (i < j) = false -> i = j.
+  (i <? j + 1) = true -> (i <? j) = false -> i = j.
 Proof.
   intros i j. rewrite ltb_spec. destruct (dec_Zlt [|i|] [|j|]) as [H|H].
   rewrite <- ltb_spec in H; rewrite H; discriminate.
@@ -86,7 +86,7 @@ Proof.
   rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. lia.
 Qed.
 
-Lemma not_0_ltb : forall x, x <> 0 <-> 0 < x = true.
+Lemma not_0_ltb : forall x, x <> 0 <-> 0 <? x = true.
 Proof.
  intros x;rewrite ltb_spec, to_Z_0;assert (W:=to_Z_bounded x);split.
  intros Hd;assert ([|x|] <> 0)%Z;[ | lia].
@@ -95,34 +95,34 @@ Proof.
  assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | lia].
 Qed.
 
-Lemma ltb_0 : forall x, ~ (x < 0 = true).
+Lemma ltb_0 : forall x, ~ (x <? 0 = true).
 Proof.
  intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);lia.
 Qed.
 
-Lemma not_ltb_refl : forall i, ~(i < i = true).
+Lemma not_ltb_refl : forall i, ~(i <? i = true).
 Proof.
  intros;rewrite ltb_spec;lia.
 Qed.
 
-Lemma ltb_trans : forall x y z, x < y = true ->  y < z = true -> x < z = true.
+Lemma ltb_trans : forall x y z, x <? y = true ->  y <? z = true -> x <? z = true.
 Proof.
  intros x y z;rewrite !ltb_spec;apply Z.lt_trans.
 Qed.
 
-Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y)).
+Lemma leb_ltb_eqb : forall x y, ((x <=? y) = (x <? y) || (x =? y)).
 Proof.
  intros.
  apply eq_true_iff_eq.
  rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;lia.
 Qed.
 
-Lemma leb_ltb_trans : forall x y z, x <= y = true ->  y < z = true -> x < z = true.
+Lemma leb_ltb_trans : forall x y z, x <=? y = true ->  y <? z = true -> x <? z = true.
 Proof.
  intros x y z;rewrite leb_spec, !ltb_spec;apply Z.le_lt_trans.
 Qed.
 
-Lemma to_Z_add_1 : forall x y, x < y = true -> [|x+1|] = ([|x|] + 1)%Z.
+Lemma to_Z_add_1 : forall x y, x <? y = true -> [|x+1|] = ([|x|] + 1)%Z.
 Proof.
   intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
    rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;lia.
@@ -133,12 +133,12 @@ Proof.
   intros; assert (Bx := to_Z_bounded x); rewrite add_spec, to_Z_1, Z.mod_small; lia.
 Qed.
 
-Lemma leb_not_gtb : forall n m, m <= n = true -> ~(n < m = true).
+Lemma leb_not_gtb : forall n m, m <=? n = true -> ~(n <? m = true).
 Proof.
  intros n m; rewrite ltb_spec, leb_spec;lia.
 Qed.
 
-Lemma leb_negb_gtb : forall x y, x <= y = negb (y < x).
+Lemma leb_negb_gtb : forall x y, x <=? y = negb (y <? x).
 Proof.
  intros x y;apply Bool.eq_true_iff_eq;split;intros.
  apply Bool.eq_true_not_negb;apply leb_not_gtb;trivial.
@@ -146,18 +146,18 @@ Proof.
  rewrite leb_spec; rewrite ltb_spec in H;lia.
 Qed.
 
-Lemma ltb_negb_geb : forall x y, x < y = negb (y <= x).
+Lemma ltb_negb_geb : forall x y, x <? y = negb (y <=? x).
 Proof.
  intros;rewrite leb_negb_gtb, Bool.negb_involutive;trivial.
 Qed.
 
-Lemma to_Z_sub_gt : forall x y, y <= x = true -> [|x - y|] = ([|x|] - [|y|])%Z.
+Lemma to_Z_sub_gt : forall x y, y <=? x = true -> [|x - y|] = ([|x|] - [|y|])%Z.
 Proof.
  intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
    rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;lia.
 Qed.
 
-Lemma to_Z_sub_1 : forall x y, y < x = true -> ([| x - 1|] = [|x|] - 1)%Z.
+Lemma to_Z_sub_1 : forall x y, y <? x = true -> ([| x - 1|] = [|x|] - 1)%Z.
 Proof.
  intros;apply to_Z_sub_gt.
  generalize (leb_ltb_trans _ _ _ (leb_0 y) H).
@@ -174,14 +174,14 @@ Proof.
  intros; apply (to_Z_sub_1 _ 0); rewrite ltb_spec; assumption.
 Qed.
 
-Lemma ltb_leb_sub1 : forall x i,  x <> 0 -> (i < x = true <-> i <= x - 1 = true).
+Lemma ltb_leb_sub1 : forall x i,  x <> 0 -> (i <? x = true <-> i <=? x - 1 = true).
 Proof.
  intros x i Hdiff.
  rewrite ltb_spec, leb_spec, to_Z_sub_1_diff;trivial.
  split;auto with zarith.
 Qed.
 
-Lemma minus_1_lt i : (i == 0) = false -> i - 1 < i = true.
+Lemma minus_1_lt i : (i =? 0) = false -> i - 1 <? i = true.
 Proof.
   intro Hl. rewrite ltb_spec, (to_Z_sub_1 _ 0).
   - lia.
@@ -203,7 +203,7 @@ Lemma lxor_lsr i1 i2 i: (i1 lxor i2) >> i = (i1 >> i) lxor (i2 >> i).
 Proof.
  apply bit_ext; intros n.
  rewrite lxor_spec, !bit_lsr, lxor_spec.
- case (_ <= _); auto.
+ case (_ <=? _); auto.
 Qed.
 
 Lemma bit_or_split i : i = (i>>1)<<1 lor bit i 0.
@@ -215,21 +215,21 @@ Proof.
  case (Zle_lt_or_eq _ _ Hi).
  2: replace 0%Z with [|0|]; auto; rewrite to_Z_eq.
  2: intros H; rewrite <-H.
- 2: replace (0 < 1) with true; auto.
+ 2: replace (0 <? 1) with true; auto.
  intros H; clear Hi.
- case_eq (n == 0).
+ case_eq (n =? 0).
  rewrite eqb_spec; intros H1; generalize H; rewrite H1; discriminate.
  intros _; rewrite orb_false_r.
- case_eq (n < 1).
+ case_eq (n <? 1).
  rewrite ltb_spec, to_Z_1; intros HH; contradict HH; auto with zarith.
  intros _.
- generalize (@bit_M i n); case (_ <= _).
+ generalize (@bit_M i n); case (_ <=? _).
  intros H1; rewrite H1; auto.
  intros _.
  case (to_Z_bounded n); intros H1n H2n.
  assert (F1: [|n - 1|] = ([|n|] - 1)%Z).
  rewrite sub_spec, Zmod_small; rewrite to_Z_1; auto with zarith.
- generalize (add_le_r 1 (n - 1)); case (_ <= _); rewrite F1, to_Z_1; intros HH.
+ generalize (add_le_r 1 (n - 1)); case (_ <=? _); rewrite F1, to_Z_1; intros HH.
  replace (1 + (n -1)) with n. change (bit i n = bit i n). reflexivity.
  apply to_Z_inj; rewrite add_spec, F1, Zmod_small; rewrite to_Z_1;
   auto with zarith.
@@ -253,10 +253,10 @@ Proof.
  assert (H1 : n = (n-1)+1).
    apply to_Z_inj;rewrite add_spec, W3.
    rewrite Zmod_small;rewrite to_Z_1; lia.
- case_eq ((n-1) < digits); intro l.
+ case_eq ((n-1) <? digits); intro l.
   rewrite ltb_spec in l.
   rewrite H1, <- !bit_half, H; trivial; rewrite ltb_spec; trivial.
- assert ((digits <= n) = true).
+ assert ((digits <=? n) = true).
   rewrite <- Bool.not_true_iff_false, ltb_spec in l; rewrite leb_spec;lia.
  rewrite !bit_M;trivial.
 Qed.
@@ -295,7 +295,7 @@ Qed.
 
 Lemma int_ind : forall (P : int -> Prop),
   P 0 ->
-  (forall i, (i < max_int) = true -> P i -> P (i + 1)) ->
+  (forall i, (i <? max_int) = true -> P i -> P (i + 1)) ->
   forall i, P i.
 Proof.
  intros P HP0 Hrec i.
@@ -327,9 +327,9 @@ Proof.
 Qed.
 
 Lemma int_ind_bounded : forall (P : int -> Prop) min max,
-  min <= max = true ->
+  min <=? max = true ->
   P min ->
-  (forall i, min <= i = true -> i < max = true -> P i -> P (i + 1)) ->
+  (forall i, min <=? i = true -> i <? max = true -> P i -> P (i + 1)) ->
   P max.
 Proof.
  intros P min max Hle Hmin Hrec.
@@ -364,7 +364,7 @@ rewrite <- to_Z_eq.
 rewrite sub_spec, to_Z_1.
 rewrite 2!bit_0_spec.
 rewrite sub_spec, to_Z_1.
-case_eq (i == 0).
+case_eq (i =? 0).
 rewrite eqb_spec; intro Hi; rewrite Hi; reflexivity.
 rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0.
 generalize (to_Z_bounded i).
@@ -442,7 +442,7 @@ Fixpoint iter_int63_aux (n : nat) (i : int) (A : Type) (f : A -> A) : A -> A :=
   match n with
   | O => fun x => x
   | S n =>
-    if i == 0 then fun x => x
+    if i =? 0 then fun x => x
     else let g := iter_int63_aux n (i >> 1) A f in
       fun x => if bit i 0 then f (g (g x)) else g (g x)
   end.
@@ -460,7 +460,7 @@ rewrite <- to_Z_eq, to_Z_0.
 generalize (to_Z_bounded i); lia.
 reflexivity.
 intros i a Hi; simpl.
-case (i == 0); [ reflexivity | ].
+case (i =? 0); [ reflexivity | ].
 rewrite IHn; [ | apply pow2_lsr; assumption].
 rewrite IHn; [ | apply pow2_lsr; assumption].
 case (bit i 0); reflexivity.
@@ -484,20 +484,20 @@ intros n i A f; revert i; induction n; intros i a Hi.
   lia.
 }
 simpl.
-replace (i == 0) with false.
+replace (i =? 0) with false.
 {
   rewrite bit_sub1_0, sub1_lsr.
   {
     case_eq (bit i 0); simpl.
     {
       intros _.
-      case_eq (i == 1).
+      case_eq (i =? 1).
       {
         rewrite eqb_spec; intro H; rewrite H in *; clear i H.
         case n; reflexivity.
       }
       rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1.
-      replace (i - 1 == 0) with false.
+      replace (i - 1 =? 0) with false.
       {
         reflexivity.
       }
@@ -505,14 +505,14 @@ replace (i == 0) with false.
       rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia.
     }
     intro Hibit.
-    case_eq (i == 1).
+    case_eq (i =? 1).
     {
       rewrite eqb_spec; intro H; rewrite H in *; clear i H; discriminate.
     }
     rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1.
-    replace (i - 1 == 0) with false.
+    replace (i - 1 =? 0) with false.
     {
-      case_eq (i == 2).
+      case_eq (i =? 2).
       {
         rewrite eqb_spec; intro H; rewrite H in *; clear i H.
         destruct n; [ lia | ].
@@ -559,7 +559,7 @@ symmetry.
 rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0; lia.
 Qed.
 
-Lemma iter_int63_S : forall i A f a, 0 < i = true -> iter_int63 i A f a = f (iter_int63 (i - 1) A f a).
+Lemma iter_int63_S : forall i A f a, 0 <? i = true -> iter_int63 i A f a = f (iter_int63 (i - 1) A f a).
 Proof.
 intros i A f a.
 rewrite ltb_spec, to_Z_0; intro Hi.
@@ -575,7 +575,7 @@ Definition foldi
      (from to : int)
      (a       : A)
        : A :=
-  if to <= from then
+  if to <=? from then
     a
   else
     let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * A)%type) =>
@@ -583,14 +583,14 @@ Definition foldi
                                       ) (from, a) in r.
 
 Lemma foldi_ge : forall A f from to (a:A),
-  to <= from = true -> foldi f from to a = a.
+  to <=? from = true -> foldi f from to a = a.
 Proof.
  intros A f from to a; unfold foldi.
  intro H; rewrite H; reflexivity.
 Qed.
 
 Lemma foldi_lt_l : forall A f from to (a:A),
-  from < to = true -> foldi f from to a = foldi f (from + 1) to (f from a).
+  from <? to = true -> foldi f from to a = foldi f (from + 1) to (f from a).
 Proof.
 intros A f from to a Hfromto.
 pose proof (to_Z_bounded from) as Hfrom.
@@ -599,7 +599,7 @@ unfold foldi.
 rewrite leb_negb_gtb.
 rewrite Hfromto; simpl.
 rewrite ltb_spec in Hfromto.
-case_eq (to <= from + 1).
+case_eq (to <=? from + 1).
 rewrite leb_spec, to_Z_add_1_wB; [ | lia ].
 intro Htofrom.
 assert (H : to = from + 1).
@@ -620,7 +620,7 @@ rewrite ltb_spec, to_Z_0, sub_spec, Zmod_small; lia.
 Qed.
 
 Lemma foldi_lt_r : forall A f from to (a:A),
-  from < to = true -> foldi f from to a = f (to - 1) (foldi f from (to - 1) a).
+  from <? to = true -> foldi f from to a = f (to - 1) (foldi f from (to - 1) a).
 Proof.
  intros A f from to a; rewrite ltb_spec; intro Hlt.
  assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to).
@@ -641,8 +641,8 @@ Proof.
 Qed.
 
 Lemma foldi_ind : forall A (P : int -> A -> Prop) f from to a,
-  from <= to = true -> P from a ->
-  (forall i a, from <= i = true -> i < to = true -> P i a -> P (i + 1) (f i a)) ->
+  from <=? to = true -> P from a ->
+  (forall i a, from <=? i = true -> i <? to = true -> P i a -> P (i + 1) (f i a)) ->
   P to (foldi f from to a).
 Proof.
   intros A P f from to a Hle Hfrom IH.
@@ -657,8 +657,8 @@ Proof.
 Qed.
 
 Lemma foldi_ind2 : forall A B (P : int -> A -> B -> Prop) f1 f2 from to a1 a2,
-  from <= to = true -> P from a1 a2 ->
-  (forall i a1 a2, from <= i = true -> i < to = true -> P i a1 a2 -> P (i + 1) (f1 i a1) (f2 i a2)) ->
+  from <=? to = true -> P from a1 a2 ->
+  (forall i a1 a2, from <=? i = true -> i <? to = true -> P i a1 a2 -> P (i + 1) (f1 i a1) (f2 i a2)) ->
   P to (foldi f1 from to a1) (foldi f2 from to a2).
 Proof.
   intros A B P f1 f2 from to a1 a2 Hle Hfrom IH.
@@ -673,7 +673,7 @@ Proof.
 Qed.
 
 Lemma foldi_eq_compat : forall A (f1 f2:int -> A -> A) min max a,
-  (forall i a, min <= i = true -> i < max = true -> f1 i a = f2 i a) ->
+  (forall i a, min <=? i = true -> i <? max = true -> f1 i a = f2 i a) ->
   foldi f1 min max a = foldi f2 min max a.
 Proof.
  intros A f1 f2 min max a Hf.
@@ -702,7 +702,7 @@ Proof.
 Qed.
 
 Lemma to_list_In : forall {A} (t: array A) i,
-  i < length t = true -> In (t.[i]) (to_list t).
+  i <? length t = true -> In (t.[i]) (to_list t).
   intros A t i; assert (Bt := to_Z_bounded (length t)); assert (Bi := to_Z_bounded i); rewrite ltb_spec; unfold to_list.
   rewrite <- in_rev.
   apply foldi_ind.
@@ -719,13 +719,13 @@ Lemma to_list_In : forall {A} (t: array A) i,
 Qed.
 
 Lemma to_list_In_eq : forall {A} (t: array A) i x,
-  i < length t = true -> x = t.[i] -> In x (to_list t).
+  i <? length t = true -> x = t.[i] -> In x (to_list t).
 Proof.
   intros A t i x Hi ->. now apply to_list_In.
 Qed.
 
 Lemma In_to_list : forall {A} (t: array A) x,
-  In x (to_list t) -> exists i, i < length t = true /\ x = t.[i].
+  In x (to_list t) -> exists i, i <? length t = true /\ x = t.[i].
 Proof.
   intros A t x; assert (Bt := to_Z_bounded (length t)); unfold to_list.
   rewrite <- in_rev.
@@ -786,7 +786,7 @@ Proof.
 Qed.
 
 Lemma get_amapi : forall {A B} (f:int -> A -> B) t i,
-  i < length t = true -> (amapi f t).[i] = f i (t.[i]).
+  i <? length t = true -> (amapi f t).[i] = f i (t.[i]).
 Proof.
   intros A B f t.
   assert (Bt := to_Z_bounded (length t)).
@@ -806,13 +806,13 @@ Proof.
 Qed.
 
 Lemma get_amap : forall {A B} (f:A -> B) t i,
-  i < length t = true -> (amap f t).[i] = f (t.[i]).
+  i <? length t = true -> (amap f t).[i] = f (t.[i]).
 Proof.
   intros; unfold amap; apply get_amapi; assumption.
 Qed.
 
 Lemma get_amapi_outofbound : forall {A B} (f:int -> A -> B) t i,
-  i < length t = false -> (amapi f t).[i] = f (length t) (default t).
+  i <? length t = false -> (amapi f t).[i] = f (length t) (default t).
 Proof.
   intros A B f t i H1; rewrite get_outofbound.
   apply default_amapi.
@@ -820,7 +820,7 @@ Proof.
 Qed.
 
 Lemma get_amap_outofbound : forall {A B} (f:A -> B) t i,
-  i < length t = false -> (amap f t).[i] = f (default t).
+  i <? length t = false -> (amap f t).[i] = f (default t).
 Proof.
   intros; unfold amap; apply get_amapi_outofbound; assumption.
 Qed.
@@ -845,7 +845,7 @@ Qed.
 (** Some properties about afold_left *)
 
 Definition afold_left A default (OP : A -> A -> A) (V : array A) :=
-  if length V == 0 then default
+  if length V =? 0 then default
   else foldi (fun i a => OP a (V.[i])) 1 (length V) (V.[0]).
 
 Lemma afold_left_spec : forall A args op (e : A),
@@ -863,7 +863,7 @@ Lemma afold_left_spec : forall A args op (e : A),
 Lemma afold_left_eq :
   forall A OP (def : A) V1 V2,
     length V1 = length V2 ->
-    (forall i, i < length V1 = true -> V1.[i] = V2.[i]) ->
+    (forall i, i <? length V1 = true -> V1.[i] = V2.[i]) ->
     afold_left _ def OP V1 = afold_left _ def OP V2.
 Proof.
   intros A OP def V1 V2 Heqlength HeqV.
@@ -885,8 +885,8 @@ Qed.
 
 Lemma afold_left_ind : forall A OP def V (P : int -> A -> Prop),
   (length V = 0 -> P 0 def) ->
-  (0 < length V = true -> P 1 (V.[0])) ->
-  (forall a i, 0 < i = true -> i < length V = true -> P i a -> P (i + 1) (OP a (V.[i]))) ->
+  (0 <? length V = true -> P 1 (V.[0])) ->
+  (forall a i, 0 <? i = true -> i <? length V = true -> P i a -> P (i + 1) (OP a (V.[i]))) ->
   P (length V) (afold_left A def OP V).
 Proof.
   intros A OP def V P HP0 HP1 HPOP.
@@ -905,7 +905,7 @@ Qed.
 (** Some properties about afold_right *)
 
 Definition afold_right A default (OP : A -> A -> A) (V : array A) :=
-  if length V == 0 then default
+  if length V =? 0 then default
   else foldi (fun i => OP (V.[length V - 1 - i])) 1 (length V) (V.[length V - 1]).
 
 Lemma afold_right_spec : forall A args op (e : A),
@@ -927,7 +927,7 @@ Lemma afold_right_spec : forall A args op (e : A),
 Lemma afold_right_eq :
   forall A OP (def : A) V1 V2,
     length V1 = length V2 ->
-    (forall i, i < length V1 = true -> V1.[i] = V2.[i]) ->
+    (forall i, i <? length V1 = true -> V1.[i] = V2.[i]) ->
     afold_right _ def OP V1 = afold_right _ def OP V2.
 Proof.
   intros A OP def V1 V2 Heqlength HeqV.
@@ -948,8 +948,8 @@ Qed.
 
 Lemma afold_right_ind : forall A OP def V (P : int -> A -> Prop),
   (length V = 0 -> P 0 def) ->
-  (0 < length V = true -> P (length V - 1) (V.[length V - 1])) ->
-  (forall a i, 0 < i = true -> i < length V = true -> P i a -> P (i - 1) (OP (V.[i - 1]) a)) ->
+  (0 <? length V = true -> P (length V - 1) (V.[length V - 1])) ->
+  (forall a i, 0 <? i = true -> i <? length V = true -> P i a -> P (i - 1) (OP (V.[i - 1]) a)) ->
   P 0 (afold_right A def OP V).
 Proof.
   intros A OP def V P HP0 HP1 HPOP.
@@ -972,7 +972,7 @@ Qed.
 (* Case andb *)
 
 Lemma afold_left_andb_false : forall i a,
-  i < length a = true ->
+  i <? length a = true ->
   a .[ i] = false ->
   afold_left bool true andb a = false.
 Proof.
@@ -991,7 +991,7 @@ Qed.
 
 Lemma afold_left_andb_false_inv : forall a,
   afold_left bool true andb a = false ->
-  exists i, (i < length a = true) /\ (a .[ i] = false).
+  exists i, (i <? length a = true) /\ (a .[ i] = false).
 Proof.
   intro a; assert (Ba := to_Z_bounded (length a)).
   rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
@@ -1008,7 +1008,7 @@ Proof.
 Qed.
 
 Lemma afold_left_andb_true : forall a,
-  (forall i, i < length a = true -> a.[i] = true) ->
+  (forall i, i <? length a = true -> a.[i] = true) ->
   afold_left bool true andb a = true.
 Proof.
   intros a H.
@@ -1020,7 +1020,7 @@ Qed.
 
 Lemma afold_left_andb_true_inv : forall a,
   afold_left bool true andb a = true ->
-  forall i, i < length a = true -> a.[i] = true.
+  forall i, i <? length a = true -> a.[i] = true.
 Proof.
   intros a H i; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i).
   revert H; rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
@@ -1052,7 +1052,7 @@ Qed.
 (* Case orb *)
 
 Lemma afold_left_orb_true : forall i a,
-  i < length a = true ->
+  i <? length a = true ->
   a .[ i] = true ->
   afold_left bool false orb a = true.
 Proof.
@@ -1071,7 +1071,7 @@ Qed.
 
 Lemma afold_left_orb_true_inv : forall a,
   afold_left bool false orb a = true ->
-  exists i, i < length a = true /\ a .[ i] = true.
+  exists i, i <? length a = true /\ a .[ i] = true.
 Proof.
   intro a; assert (Ba := to_Z_bounded (length a)).
   rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
@@ -1088,7 +1088,7 @@ Proof.
 Qed.
 
 Lemma afold_left_orb_false : forall a,
-  (forall i, i < length a = true -> a.[i] = false) ->
+  (forall i, i <? length a = true -> a.[i] = false) ->
   afold_left bool false orb a = false.
 Proof.
   intros a H.
@@ -1100,7 +1100,7 @@ Qed.
 
 Lemma afold_left_orb_false_inv : forall a,
   afold_left bool false orb a = false ->
-  forall i, i < length a = true -> a.[i] = false.
+  forall i, i <? length a = true -> a.[i] = false.
 Proof.
   intros a H i; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i).
   revert H; rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
@@ -1132,8 +1132,8 @@ Qed.
 (* Case implb *)
 
 Lemma afold_right_implb_false : forall a,
-  0 < length a = true /\
-  (forall i, i < length a - 1 = true -> a .[ i] = true) /\
+  0 <? length a = true /\
+  (forall i, i <? length a - 1 = true -> a .[ i] = true) /\
   a.[length a - 1] = false ->
   afold_right bool true implb a = false.
 Proof.
@@ -1150,8 +1150,8 @@ Qed.
 
 Lemma afold_right_implb_false_inv : forall a,
   afold_right bool true implb a = false ->
-  0 < length a = true /\
-  (forall i, i < length a - 1 = true -> a .[ i] = true) /\
+  0 <? length a = true /\
+  (forall i, i <? length a - 1 = true -> a .[ i] = true) /\
   a.[length a - 1] = false.
 Proof.
   intros a H; assert (Ba := to_Z_bounded (length a)); split; [ | split ].
@@ -1185,7 +1185,7 @@ Proof.
 Qed.
 
 Lemma afold_right_implb_true_aux : forall a,
-  (exists i, i < length a - 1 = true /\ a.[i] = false) ->
+  (exists i, i <? length a - 1 = true /\ a.[i] = false) ->
   afold_right bool true implb a = true.
 Proof.
   intros a [ i [ Hi Hai ] ].
@@ -1206,8 +1206,8 @@ Proof.
 Qed.
 
 Lemma afold_right_implb_true : forall a,
-  length a = 0 \/ (exists i, i < length a - 1 = true /\ a.[i] = false) \/
-  (forall i, i < length a = true -> a.[i] = true) ->
+  length a = 0 \/ (exists i, i <? length a - 1 = true /\ a.[i] = false) \/
+  (forall i, i <? length a = true -> a.[i] = true) ->
   afold_right bool true implb a = true.
 Proof.
   intro a; assert (Ba := to_Z_bounded (length a)); case (reflect_eqb (length a) 0).
@@ -1216,7 +1216,7 @@ Proof.
   intros [H1|[H1|H1]].
   elim (Hneq H1).
   apply afold_right_implb_true_aux; auto.
-  assert (Heq : length a == 0 = false) by (rewrite <- not_true_iff_false, eqb_spec; exact Hneq).
+  assert (Heq : length a =? 0 = false) by (rewrite <- not_true_iff_false, eqb_spec; exact Hneq).
   unfold afold_right; rewrite Heq.
   revert Hneq; rewrite <- to_Z_eq, to_Z_0; intro Hneq.
   apply (foldi_ind _ (fun i a => a = true)).
@@ -1230,12 +1230,12 @@ Qed.
 
 Lemma afold_right_implb_true_inv : forall a,
   afold_right bool true implb a = true ->
-  length a = 0 \/ (exists i, i < length a - 1 = true /\ a.[i] = false) \/
-  (forall i, i < length a = true -> a.[i] = true).
+  length a = 0 \/ (exists i, i <? length a - 1 = true /\ a.[i] = false) \/
+  (forall i, i <? length a = true -> a.[i] = true).
 Proof.
   intros a H; cut (length a = 0
-    \/ (exists i, 0 <= i = true /\ i < length a - 1 = true /\ a.[i] = false)
-    \/ (forall i, 0 <= i = true -> i < length a = true -> a.[i] = true)).
+    \/ (exists i, 0 <=? i = true /\ i <? length a - 1 = true /\ a.[i] = false)
+    \/ (forall i, 0 <=? i = true -> i <? length a = true -> a.[i] = true)).
   clear H; intro H; destruct H as [ H | H ].
   left; tauto.
   destruct H as [ H | H ].
@@ -1276,18 +1276,18 @@ Qed.
 (* Other cases *)
 
 Lemma afold_left_length_2 : forall A default OP t,
-  (length t == 2) = true ->
+  (length t =? 2) = true ->
   afold_left A default OP t = OP (t.[0]) (t.[1]).
 Proof.
-  intros A default OP t H; unfold afold_left; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; reflexivity.
+  intros A default OP t H; unfold afold_left; rewrite eqb_spec in H; rewrite H; change (2 =? 0) with false; reflexivity.
 Qed.
 
 
 Lemma afold_right_length_2 : forall A default OP t,
-  (length t == 2) = true ->
+  (length t =? 2) = true ->
   afold_right A default OP t = OP (t.[0]) (t.[1]).
 Proof.
-  intros A default OP t H; unfold afold_right; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; reflexivity.
+  intros A default OP t H; unfold afold_right; rewrite eqb_spec in H; rewrite H; change (2 =? 0) with false; reflexivity.
 Qed.
 
 
@@ -1305,77 +1305,77 @@ Ltac tac_right :=
 
 
 Lemma afold_left_xorb_false1 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = false -> t .[ 1] = false ->
   afold_left bool false xorb t = false.
 Proof. tac_left. Qed.
 
 
 Lemma afold_left_xorb_false2 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = true -> t .[ 1] = true ->
   afold_left bool false xorb t = false.
 Proof. tac_left. Qed.
 
 
 Lemma afold_left_xorb_true1 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = false -> t .[ 1] = true ->
   afold_left bool false xorb t = true.
 Proof. tac_left. Qed.
 
 
 Lemma afold_left_xorb_true2 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = true -> t .[ 1] = false ->
   afold_left bool false xorb t = true.
 Proof. tac_left. Qed.
 
 
 (* Lemma afold_right_implb_false : forall t f, *)
-(*   (PArray.length t == 2) = true -> *)
+(*   (PArray.length t =? 2) = true -> *)
 (*   f (t .[ 0]) = true -> f (t .[ 1]) = false -> *)
 (*   afold_right bool int true implb f t = false. *)
 (* Proof. tac_right. Qed. *)
 
 
 (* Lemma afold_right_implb_true1 : forall t f, *)
-(*   (PArray.length t == 2) = true -> *)
+(*   (PArray.length t =? 2) = true -> *)
 (*   f (t .[ 0]) = false -> *)
 (*   afold_right bool int true implb f t = true. *)
 (* Proof. tac_right. Qed. *)
 
 
 (* Lemma afold_right_implb_true2 : forall t f, *)
-(*   (PArray.length t == 2) = true -> *)
+(*   (PArray.length t =? 2) = true -> *)
 (*   f (t.[1]) = true -> *)
 (*   afold_right bool int true implb f t = true. *)
 (* Proof. tac_right. Qed. *)
 
 
 Lemma afold_left_eqb_false1 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = false -> t .[ 1] = true ->
   afold_left bool true eqb t = false.
 Proof. tac_left. Qed.
 
 
 Lemma afold_left_eqb_false2 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = true -> t .[ 1] = false ->
   afold_left bool true eqb t = false.
 Proof. tac_left. Qed.
 
 
 Lemma afold_left_eqb_true1 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = true -> t .[ 1] = true ->
   afold_left bool true eqb t = true.
 Proof. tac_left. Qed.
 
 
 Lemma afold_left_eqb_true2 : forall t,
-  (PArray.length t == 2) = true ->
+  (PArray.length t =? 2) = true ->
   t .[ 0] = false -> t .[ 1] = false ->
   afold_left bool true eqb t = true.
 Proof. tac_left. Qed.
@@ -1573,7 +1573,7 @@ Definition aexistsbi {A:Type} (f:int->A->bool) (t:array A) :=
 
 Lemma aexistsbi_false_spec : forall A (f : int -> A -> bool) t,
   aexistsbi f t = false <->
-  forall i, i < length t = true -> f i (t.[i]) = false.
+  forall i, i <? length t = true -> f i (t.[i]) = false.
 Proof.
   intros A f t; unfold aexistsbi.
   split.
@@ -1586,7 +1586,7 @@ Proof.
 Qed.
 
 Lemma aexistsbi_spec : forall A (f : int -> A -> bool) t,
-  aexistsbi f t = true <-> exists i, i < length t = true /\ f i (t.[i]) = true.
+  aexistsbi f t = true <-> exists i, i <? length t = true /\ f i (t.[i]) = true.
 Proof.
   intros A f t; unfold aexistsbi.
   split.
@@ -1602,7 +1602,7 @@ Definition aforallbi {A:Type} (f:int->A->bool) (t:array A) :=
   afold_left _ true andb (amapi f t).
 
 Lemma aforallbi_false_spec : forall A (f : int -> A -> bool) t,
-  aforallbi f t = false <-> exists i, i < length t = true /\ f i (t.[i]) = false.
+  aforallbi f t = false <-> exists i, i <? length t = true /\ f i (t.[i]) = false.
 Proof.
   intros A f t; unfold aforallbi.
   split.
@@ -1616,7 +1616,7 @@ Qed.
 
 Lemma aforallbi_spec : forall A (f : int -> A -> bool) t,
   aforallbi f t = true <->
-  forall i, i < length t = true -> f i (t.[i]) = true.
+  forall i, i <? length t = true -> f i (t.[i]) = true.
 Proof.
   intros A f t; unfold aforallbi.
   split.
diff --git a/src/PArray/PArray.v b/src/PArray/PArray.v
index 03f1abd..891db84 100644
--- a/src/PArray/PArray.v
+++ b/src/PArray/PArray.v
@@ -27,9 +27,9 @@ Module IntOrderedType <: OrderedType.
 
   Definition t := int.
 
-  Definition eq x y := (x == y) = true.
+  Definition eq x y := (x =? y) = true.
 
-  Definition lt x y := (x < y) = true.
+  Definition lt x y := (x <? y) = true.
 
   Lemma eq_refl x : eq x x.
   Proof. unfold eq. rewrite eqb_spec. reflexivity. Qed.
@@ -48,9 +48,9 @@ Module IntOrderedType <: OrderedType.
 
   Definition compare x y : Compare lt eq x y.
   Proof.
-    case_eq (x < y); intro e.
+    case_eq (x <? y); intro e.
       exact (LT e).
-      case_eq (x == y); intro e2.
+      case_eq (x =? y); intro e2.
         exact (EQ e2).
         apply GT. unfold lt.
         rewrite <- Bool.not_false_iff_true, <- Bool.not_true_iff_false, ltb_spec, eqb_spec in *; intro e3.
@@ -59,7 +59,7 @@ Module IntOrderedType <: OrderedType.
 
   Definition eq_dec x y : { eq x y } + { ~ eq x y }.
   Proof.
-    case_eq (x == y); intro e.
+    case_eq (x =? y); intro e.
       left; exact e.
       right. intro H. rewrite H in e. discriminate.
   Defined.
@@ -78,7 +78,7 @@ Definition make {A:Type} (l:int) (d:A) : array A := (Map.empty A, d, l).
 Definition get {A:Type} (t:array A) (i:int) : A :=
   let (td, l) := t in
   let (t, d) := td in
-  if i < l then
+  if i <? l then
     match Map.find i t with
       | Some x => x
       | None => d
@@ -90,7 +90,7 @@ Definition default {A:Type} (t:array A) : A :=
 
 Definition set {A:Type} (t:array A) (i:int) (a:A) : array A :=
   let (td,l) := t in
-  if l <= i then
+  if l <=? i then
     t
   else
     let (t,d) := td in
@@ -115,14 +115,14 @@ Definition max_length := max_int.
 Require FSets.FMapFacts.
 Module P := FSets.FMapFacts.WProperties_fun IntOrderedType Map.
 
-Lemma get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t.
+Lemma get_outofbound : forall A (t:array A) i, (i <? length t) = false -> t.[i] = default t.
 intros A t i; unfold get.
 destruct t as ((t, d), l).
 unfold length; intro Hi; rewrite Hi; clear Hi.
 reflexivity.
 Qed.
 
-Lemma get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
+Lemma get_set_same : forall A t i (a:A), (i <? length t) = true -> t.[i<-a].[i] = a.
 intros A t i a.
 destruct t as ((t, d), l).
 unfold set, get, length.
@@ -143,7 +143,7 @@ Lemma get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
 intros A t i j a Hij.
 destruct t as ((t, d), l).
 unfold set, get, length.
-case (l <= i).
+case (l <=? i).
 reflexivity.
 rewrite P.F.add_neq_o.
 reflexivity.
@@ -156,17 +156,17 @@ Lemma default_set : forall A t i (a:A), default (t.[i<-a]) = default t.
 intros A t i a.
 destruct t as ((t, d), l).
 unfold default, set.
-case (l <= i); reflexivity.
+case (l <=? i); reflexivity.
 Qed.
 
 Lemma get_make : forall A (a:A) size i, (make size a).[i] = a.
 intros A a size i.
 unfold make, get.
 rewrite P.F.empty_o.
-case (i < size); reflexivity.
+case (i <? size); reflexivity.
 Qed.
 
-Lemma leb_length : forall A (t:array A), length t <= max_length = true.
+Lemma leb_length : forall A (t:array A), length t <=? max_length = true.
 intros A t.
 generalize (length t); clear t.
 intro i.
@@ -177,10 +177,10 @@ apply to_Z_bounded.
 Qed.
 
 Lemma length_make : forall A size (a:A),
-  length (make size a) = if size <= max_length then size else max_length.
+  length (make size a) = if size <=? max_length then size else max_length.
 intros A size a.
 unfold length, make.
-replace (size <= max_length) with true.
+replace (size <=? max_length) with true.
 reflexivity.
 symmetry.
 rewrite leb_spec.
@@ -194,7 +194,7 @@ Lemma length_set : forall A t i (a:A),
 intros A t i a.
 destruct t as ((t, d), l).
 unfold length, set.
-case (l <= i); reflexivity.
+case (l <=? i); reflexivity.
 Qed.
 
 Lemma get_copy : forall A (t:array A) i, (copy t).[i] = t.[i].
@@ -211,7 +211,7 @@ Qed.
 (*
 Axiom array_ext : forall A (t1 t2:array A),
   length t1 = length t2 ->
-  (forall i, i < length t1 = true -> t1.[i] = t2.[i]) ->
+  (forall i, i <? length t1 = true -> t1.[i] = t2.[i]) ->
   default t1 = default t2 ->
   t1 = t2.
 *)
@@ -229,7 +229,7 @@ Qed.
 Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t.
 unfold default, get, set.
 destruct t as ((t, d), l).
-case_eq (i < l).
+case_eq (i <? l).
 intro H; generalize H.
 rewrite ltb_spec.
 rewrite Z.lt_nge.
@@ -252,10 +252,10 @@ reflexivity.
 Qed.
 
 Lemma get_not_default_lt A (t:array A) x :
- t.[x] <> default t -> (x < length t) = true.
+ t.[x] <> default t -> (x <? length t) = true.
 unfold get, default, length.
 destruct t as ((t, d), l).
-case (x < l); tauto.
+case (x <? l); tauto.
 Qed.
 
 (* 
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 77dc21f..b19f106 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -108,17 +108,17 @@ Module Form.
       Definition lt_form i h :=
         match h with
         | Fatom _ | Ftrue | Ffalse => true
-        | Fnot2 _ l => Lit.blit l < i
+        | Fnot2 _ l => Lit.blit l <? i
         | Fand args | For args | Fimp args =>
-          aforallbi (fun _ l => Lit.blit l < i) args
-        | Fxor a b | Fiff a b => (Lit.blit a < i) && (Lit.blit b < i)
-        | Fite a b c => (Lit.blit a < i) && (Lit.blit b < i) && (Lit.blit c < i)
-        | FbbT _ ls => List.forallb (fun l => Lit.blit l < i) ls
+          aforallbi (fun _ l => Lit.blit l <? i) args
+        | Fxor a b | Fiff a b => (Lit.blit a <? i) && (Lit.blit b <? i)
+        | Fite a b c => (Lit.blit a <? i) && (Lit.blit b <? i) && (Lit.blit c <? i)
+        | FbbT _ ls => List.forallb (fun l => Lit.blit l <? i) ls
         end.
 
       Lemma lt_form_interp_form_aux :
         forall f1 f2 i h,
-          (forall j, j < i -> f1 j = f2 j) ->
+          (forall j, j <? i -> f1 j = f2 j) ->
           lt_form i h ->
           interp_aux f1 h = interp_aux f2 h.
       Proof.
@@ -161,11 +161,11 @@ Module Form.
         intros;rewrite default_set;trivial.
       Qed.
 
-      Lemma t_interp_wf : forall i, i < PArray.length t_form ->
+      Lemma t_interp_wf : forall i, i <? PArray.length t_form ->
         t_interp.[i] = interp_aux (PArray.get t_interp) (t_form.[i]).
       Proof.
         set (P' i t := length t = length t_form ->
-          forall j, j < i ->
+          forall j, j <? i ->
             t.[j] = interp_aux (PArray.get t) (t_form.[j])).
         assert (P' (length t_form) t_interp).
         unfold is_true, wf in wf_t_i;rewrite aforallbi_spec in wf_t_i.
@@ -179,7 +179,7 @@ Module Form.
         intros;rewrite get_set_other;trivial.
         intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial.
         rewrite H2;trivial.
-        assert (j < i).
+        assert (j <? i).
         assert ([|j|] <> [|i|]) by (intros Heq1;elim n;apply to_Z_inj;trivial).
         generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0);
           auto with zarith.
@@ -203,7 +203,7 @@ Module Form.
 
     Lemma wf_interp_form_lt :
       forall t_form, wf t_form ->
-        forall x, x < PArray.length t_form ->
+        forall x, x <? PArray.length t_form ->
           interp_state_var t_form x = interp t_form (t_form.[x]).
     Proof.
       unfold interp_state_var;intros.
@@ -214,7 +214,7 @@ Module Form.
       forall t_form, PArray.default t_form = Ftrue -> wf t_form ->
         forall x, interp_state_var t_form x = interp t_form (t_form.[x]).
     Proof.
-      intros t Hd Hwf x;case_eq (x < PArray.length t);intros.
+      intros t Hd Hwf x;case_eq (x <? PArray.length t);intros.
       apply wf_interp_form_lt;trivial.
       unfold interp_state_var;rewrite !PArray.get_outofbound;trivial.
       rewrite default_t_interp, Hd;trivial.
@@ -834,12 +834,12 @@ Module Atom.
   Definition eqb (t t':atom) :=
     match t,t' with
     | Acop o, Acop o' => cop_eqb o o'
-    | Auop o t, Auop o' t' => uop_eqb o o' && (t == t')
-    | Abop o t1 t2, Abop o' t1' t2' => bop_eqb o o' && (t1 == t1') && (t2 == t2')
+    | Auop o t, Auop o' t' => uop_eqb o o' && (t =? t')
+    | Abop o t1 t2, Abop o' t1' t2' => bop_eqb o o' && (t1 =? t1') && (t2 =? t2')
     | Anop o t, Anop o' t' => nop_eqb o o' && list_beq Int63.eqb t t'
     | Atop o t1 t2 t3, Atop o' t1' t2' t3' =>
-      top_eqb o o' && (t1 == t1') && (t2 == t2') && (t3 == t3')
-    | Aapp a la, Aapp b lb => (a == b) && list_beq Int63.eqb la lb
+      top_eqb o o' && (t1 =? t1') && (t2 =? t2') && (t3 =? t3')
+    | Aapp a la, Aapp b lb => (a =? b) && list_beq Int63.eqb la lb
     | _, _ => false
     end.
 
@@ -2226,15 +2226,15 @@ Qed.
       Definition lt_atom i a :=
         match a with
         | Acop _ => true
-        | Auop _ h => h < i
-        | Abop _ h1 h2 => (h1 < i) && (h2 < i)
-        | Atop _ h1 h2 h3 => (h1 < i) && (h2 < i) && (h3 < i)
-        | Anop _ ha => List.forallb (fun h => h < i) ha
-        | Aapp f args => List.forallb (fun h => h < i) args
+        | Auop _ h => h <? i
+        | Abop _ h1 h2 => (h1 <? i) && (h2 <? i)
+        | Atop _ h1 h2 h3 => (h1 <? i) && (h2 <? i) && (h3 <? i)
+        | Anop _ ha => List.forallb (fun h => h <? i) ha
+        | Aapp f args => List.forallb (fun h => h <? i) args
         end.
 
       Lemma lt_interp_aux :
-         forall f1 f2 i, (forall j, j < i -> f1 j = f2 j) ->
+         forall f1 f2 i, (forall j, j <? i -> f1 j = f2 j) ->
          forall a, lt_atom i a ->
              interp_aux f1 a = interp_aux f2 a.
       Proof.
@@ -2277,12 +2277,12 @@ Qed.
         intros;rewrite default_set;trivial.
       Qed.
 
-      Lemma t_interp_wf_lt : forall i, i < PArray.length t_atom ->
+      Lemma t_interp_wf_lt : forall i, i <? PArray.length t_atom ->
          t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
       Proof.
         assert (Bt := to_Z_bounded (length t_atom)).
         set (P' i t := length t = length t_atom ->
-               forall j, j < i ->
+               forall j, j <? i ->
                t.[j] = interp_aux (PArray.get t) (t_atom.[j])).
         assert (P' (length t_atom) t_interp).
          unfold is_true, wf in wf_t_i;rewrite aforallbi_spec in wf_t_i.
@@ -2296,7 +2296,7 @@ Qed.
           intros;rewrite get_set_other;trivial.
           intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial.
           rewrite H2;trivial.
-         assert (j < i).
+         assert (j <? i).
           assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial).
           generalize H3;unfold is_true;rewrite !ltb_spec,
             (to_Z_add_1 _ _ H0);auto with zarith.
@@ -2313,7 +2313,7 @@ Qed.
       Lemma t_interp_wf : forall i,
          t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
       Proof.
-        intros i;case_eq (i< PArray.length t_atom);intros.
+        intros i;case_eq (i <? PArray.length t_atom);intros.
         apply t_interp_wf_lt;trivial.
         rewrite !PArray.get_outofbound;trivial.
         rewrite default_t_atom, default_t_interp;trivial.
@@ -2328,10 +2328,10 @@ Qed.
 
       Lemma check_aux_interp_aux_lt_aux : forall a h,
         (forall j : int,
-          j < h ->
+          j <? h ->
           exists v : interp_t (v_type Typ.type interp_t (a .[ j])),
             a .[ j] = Bval (v_type Typ.type interp_t (a .[ j])) v) ->
-        forall l, List.forallb (fun h0 : int => h0 < h) l = true ->
+        forall l, List.forallb (fun h0 : int => h0 <? h) l = true ->
           forall (f0: tval),
             exists
               v : interp_t
@@ -2356,9 +2356,9 @@ Qed.
         exists true; auto.
       Qed.
 
-      Lemma check_aux_interp_aux_lt : forall h, h < length t_atom ->
+      Lemma check_aux_interp_aux_lt : forall h, h <? length t_atom ->
         forall a,
-          (forall j, j < h ->
+          (forall j, j <? h ->
             exists v, a.[j] = Bval (v_type _ _ (a.[j])) v) ->
           exists v, interp_aux (get a) (t_atom.[h]) =
             Bval (v_type _ _ (interp_aux (get a) (t_atom.[h]))) v.
@@ -2485,19 +2485,19 @@ Qed.
              (k3 (Typ.interp t_i) z)); auto.
 
         (* N-ary operators *)
-        intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 < h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl.
+        intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 <? h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl.
         intros acc _; exists (distinct (Typ.i_eqb t_i A) (rev acc)); auto.
         intro acc; rewrite andb_true_iff; intros [H1 H2]; destruct (IH _ H1) as [va Hva]; rewrite Hva; simpl; case (Typ.cast (v_type Typ.type interp_t (a .[ i])) A); simpl; try (exists true; auto); intro k; destruct (IHl (k interp_t va :: acc) H2) as [vb Hvb]; exists vb; auto.
         (* Application *)
         intros i l H; apply (check_aux_interp_aux_lt_aux a h IH l H (t_func.[i])).
 Qed.
 
-      Lemma check_aux_interp_hatom_lt : forall h, h < length t_atom ->
+      Lemma check_aux_interp_hatom_lt : forall h, h <? length t_atom ->
         exists v, t_interp.[h] = Bval (get_type h) v.
       Proof.
         assert (Bt := to_Z_bounded (length t_atom)).
         set (P' i t := length t = length t_atom ->
-          forall j, j < i ->
+          forall j, j <? i ->
             exists v, t.[j] = Bval (v_type Typ.type interp_t (t.[j])) v).
         assert (P' (length t_atom) t_interp).
         unfold t_interp;apply foldi_ind;unfold P';intros.
@@ -2508,7 +2508,7 @@ Qed.
         rewrite e, PArray.get_set_same.
         apply check_aux_interp_aux_lt; auto.
         rewrite H2; auto.
-        assert (j < i).
+        assert (j <? i).
         assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial).
         generalize H3;unfold is_true;rewrite !ltb_spec,
           (to_Z_add_1 _ _ H0);auto with zarith.
@@ -2519,7 +2519,7 @@ Qed.
       Lemma check_aux_interp_hatom : forall h,
         exists v, t_interp.[h] = Bval (get_type h) v.
       Proof.
-        intros i;case_eq (i< PArray.length t_atom);intros.
+        intros i;case_eq (i <? PArray.length t_atom);intros.
         apply check_aux_interp_hatom_lt;trivial.
         unfold get_type'; rewrite !PArray.get_outofbound;trivial.
         rewrite default_t_interp; simpl; exists (1%positive); auto.
diff --git a/src/State.v b/src/State.v
index 8b899f1..4b4183b 100644
--- a/src/State.v
+++ b/src/State.v
@@ -80,7 +80,7 @@ Module Lit.
   Lemma lit_false : _false = lit Var._false.
   Proof. reflexivity. Qed.
 
-  Definition eqb (l l' : _lit) := l == l'.
+  Definition eqb (l l' : _lit) := l =? l'.
   (* Register eqb as PrimInline. *)
 
   Lemma eqb_spec : forall l l', eqb l l' = true <-> l = l'.
@@ -217,7 +217,7 @@ Module Lit.
     unfold interp, Var.interp;intros rho1 rho2 l Heq;rewrite Heq;trivial.
   Qed.
 
-  Lemma lxor_neg : forall l1 l2, (l1 lxor l2 == 1) = true -> l1 = Lit.neg l2.
+  Lemma lxor_neg : forall l1 l2, (l1 lxor l2 =? 1) = true -> l1 = Lit.neg l2.
   Proof.
     unfold Lit.neg; intros l1 l2;rewrite eqb_spec;intros Heq;rewrite <- Heq.
     rewrite lxorC, <- lxorA, lxor_nilpotent, lxor0_r;trivial.
@@ -228,14 +228,14 @@ End Lit.
 
 Lemma compare_spec' : forall x y,
     match x ?= y with
-    | Lt => x < y
+    | Lt => x <? y
     | Eq => x = y
-    | Gt => y < x
+    | Gt => y <? x
     end.
 Proof.
   intros x y;rewrite compare_def_spec;unfold compare_def.
-  case_eq (x < y);intros;[reflexivity | ].
-  case_eq (x == y);intros.
+  case_eq (x <? y);intros;[reflexivity | ].
+  case_eq (x =? y);intros.
   rewrite <- eqb_spec;trivial.
   rewrite <- not_true_iff_false in H, H0.
   unfold is_true in *;rewrite ltb_spec in H |- *;rewrite eqb_spec in H0.
@@ -264,7 +264,7 @@ Module C.
   Fixpoint has_true (c:t) :=
     match c with
       | nil => false
-      | l :: c => (l == Lit._true) || has_true c
+      | l :: c => (l =? Lit._true) || has_true c
     end.
   
 
@@ -343,9 +343,9 @@ Module C.
       | l2::c2' =>
         match compare l1 l2 with
         | Eq => l1 :: resolve c1 c2'
-        | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2
+        | Lt => if l1 lxor l2 =? 1 then or c1 c2' else l1 :: resolve c1 c2
         | Gt =>
-          if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux c2'
+          if l1 lxor l2 =? 1 then or c1 c2' else l2 :: resolve_aux c2'
         end
       end.
 
@@ -359,13 +359,13 @@ Module C.
       induction c2;simpl;try discriminate.
       generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl.
       simpl in Hc1;destruct (Lit.interp rho l1);simpl in *;auto.
-      generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros.
+      generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros.
       rewrite or_correct.
       rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a).
       simpl in Hc1;rewrite Hc1;trivial.
       simpl in H0;rewrite H0, orb_true_r;trivial.
       simpl;destruct (Lit.interp rho l1);simpl;auto.
-      generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros.
+      generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros.
       rewrite or_correct.
       rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a).
       simpl in Hc1;rewrite Hc1;trivial.
@@ -382,9 +382,9 @@ Module C.
     | l1::c1, l2::c2' =>
       match compare l1 l2 with
       | Eq => l1 :: resolve c1 c2'
-      | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2
+      | Lt => if l1 lxor l2 =? 1 then or c1 c2' else l1 :: resolve c1 c2
       | Gt =>
-        if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux resolve l1 c1 c2'
+        if l1 lxor l2 =? 1 then or c1 c2' else l2 :: resolve_aux resolve l1 c1 c2'
       end
     end.
 
@@ -397,13 +397,13 @@ Module C.
     intros Hc1 Hc2.
     generalize (compare_spec' a i);destruct (a ?= i);intros;subst;simpl.
     destruct (Lit.interp rho i);simpl in *;auto.
-    generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros.
+    generalize (Lit.lxor_neg a i);destruct (a lxor i =? 1);intros.
     rewrite or_correct.
     rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i).
     simpl in Hc1;rewrite Hc1;trivial.
     simpl in Hc2;rewrite Hc2, orb_true_r;trivial.
     simpl;destruct (Lit.interp rho a);simpl;auto.
-    generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros.
+    generalize (Lit.lxor_neg a i);destruct (a lxor i =? 1);intros.
     rewrite or_correct.
     rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i).
     simpl in Hc1;rewrite Hc1;trivial.
@@ -485,7 +485,7 @@ Module S.
   Proof.
     unfold valid, get;simpl;intros.
     destruct (reflect_eqb id id0);subst.
-    case_eq (id0 < length s);intros.
+    case_eq (id0 <? length s);intros.
     rewrite PArray.get_set_same;trivial.
     rewrite PArray.get_outofbound.
     rewrite PArray.default_set.
@@ -505,9 +505,9 @@ Module S.
    | nil => l1:: nil
    | l2 :: c' =>
      match l1 ?= l2 with
-     | Lt => if l1 lxor l2 == 1 then C._true else l1 :: c
+     | Lt => if l1 lxor l2 =? 1 then C._true else l1 :: c
      | Eq => c
-     | Gt => if l1 lxor l2 == 1 then C._true else l2 :: insert l1 c'
+     | Gt => if l1 lxor l2 =? 1 then C._true else l2 :: insert l1 c'
      end
    end.
 
@@ -558,10 +558,10 @@ Module S.
     intros rho Hwf l1;induction c;simpl;trivial.
     generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl.
     destruct (Lit.interp rho a);simpl in *;auto.
-    generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros;trivial.
+    generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros;trivial.
     rewrite C.interp_true;trivial.
     rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial.
-    generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros.
+    generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a =? 1);intros.
     rewrite C.interp_true;trivial.
     rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial.
     simpl;rewrite orb_assoc,(orb_comm (Lit.interp rho l1)),<-orb_assoc,IHc;trivial.
@@ -623,7 +623,7 @@ Module S.
   Proof.
     unfold valid, get, set_clause. intros rho s Hrho Hs pos c Hc id.
     destruct (reflect_eqb pos id);subst.
-    case_eq (id < length s); intro H.
+    case_eq (id <? length s); intro H.
     unfold get;rewrite PArray.get_set_same; trivial.
     unfold C.valid;rewrite sort_correct;trivial.
     generalize (Hs id);rewrite !PArray.get_outofbound, PArray.default_set;trivial.
@@ -641,7 +641,7 @@ Module S.
   Proof.
     unfold valid, get, set_clause_keep. intros rho s Hrho Hs pos c Hc id.
     destruct (reflect_eqb pos id);subst.
-    case_eq (id < length s); intro H.
+    case_eq (id <? length s); intro H.
     unfold get;rewrite PArray.get_set_same; trivial.
     unfold C.valid;rewrite sort_keep_correct;trivial.
     generalize (Hs id);rewrite !PArray.get_outofbound, PArray.default_set;trivial.
@@ -655,7 +655,7 @@ Module S.
 
   Definition set_resolve (s:t) pos (r:resolution) : t :=
     let len := PArray.length r in
-    if len == 0 then s
+    if len =? 0 then s
     else
       let c := foldi (fun i c' => (C.resolve (get s (r.[i])) c')) 1 len (get s (r.[0])) in
       (* S.set_clause *) internal_set s pos c.
@@ -683,8 +683,8 @@ Module S.
 
   Definition subclause (cl1 cl2 : list _lit) :=
     List.forallb (fun l1 =>
-                    (l1 == Lit._false) || (l1 == Lit.neg Lit._true) ||
-                    List.existsb (fun l2 => l1 == l2) cl2) cl1.
+                    (l1 =? Lit._false) || (l1 =? Lit.neg Lit._true) ||
+                    List.existsb (fun l2 => l1 =? l2) cl2) cl1.
   
   Definition check_weaken (s:t) (cid:clause_id) (cl:list _lit) : C.t :=
     if subclause (get s cid) cl then cl else C._true.
diff --git a/src/Trace.v b/src/Trace.v
index 1849c44..ad4c41e 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -61,7 +61,7 @@ Section trace.
       end) s a) (inl s) t in
     s'.
   Definition _checker_partial_ (s: S.t) (t: _trace_) (max:int) : S.t :=
-    PArray.fold_left (fun s a => PArray.foldi_left (fun i s' a' => if i < max then check_step s' a' else s') s a) s t.
+    PArray.fold_left (fun s a => PArray.foldi_left (fun i s' a' => if i <? max then check_step s' a' else s') s a) s t.
   *)
 
   (* Proof of its partial correction: if it returns true, then the
@@ -137,7 +137,7 @@ Qed.
 
  Lemma valid_spec : forall rho d,
    valid rho d <->
-   (forall i : int, i < length d -> C.interp rho (to_list (d.[i]))).
+   (forall i : int, i <? length d -> C.interp rho (to_list (d.[i]))).
  Proof.
    unfold valid; intros rho d; split; intro H.
    intros i Hi; case_eq (C.interp rho (to_list (d .[ i]))); try reflexivity.
@@ -210,7 +210,7 @@ Module Cnf_Checker.
 
   Local Open Scope list_scope.
 
-  Local Notation check_flatten t_form := (check_flatten t_form (fun i1 i2 => i1 == i2) (fun _ _ => false)) (only parsing).
+  Local Notation check_flatten t_form := (check_flatten t_form (fun i1 i2 => i1 =? i2) (fun _ _ => false)) (only parsing).
 
   Definition step_checker t_form s (st:step) :=
     match st with
@@ -290,7 +290,7 @@ Module Cnf_Checker.
  Definition checker_eq t_form l1 l2 l (c:certif) :=
    negb (Lit.is_pos l) &&
    match t_form.[Lit.blit l] with
-   | Form.Fiff l1' l2' => (l1 == l1') && (l2 == l2')
+   | Form.Fiff l1' l2' => (l1 =? l1') && (l2 =? l2')
    | _ => false
    end &&
    checker t_form l c.
@@ -504,7 +504,7 @@ Inductive step :=
   Definition add_roots s d used_roots :=
     match used_roots with
       | Some ur => foldi (fun i s =>
-        let c := if (ur.[i]) < length d then (d.[ur.[i]])::nil else C._true in
+        let c := if (ur.[i]) <? length d then (d.[ur.[i]])::nil else C._true in
           S.set_clause s i c) 0 (length ur) s
       | None => foldi (fun i s => S.set_clause s i (d.[i]::nil)) 0 (length d) s
     end.
@@ -521,7 +521,7 @@ Inductive step :=
         S.valid rho (add_roots s d used_roots).
   Proof.
     intros (* t_i t_func t_atom t_form *) rho H1 H2 H10 s d used_roots H3; unfold valid; intro H4; pose (H5 := (afold_left_andb_true_inv _ H4)); unfold add_roots; assert (Valuation.wf rho) by (destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H]; auto with smtcoq_core); case used_roots.
-    intro ur; apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; case_eq (ur .[ i] < length d).
+    intro ur; apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; case_eq (ur .[ i] <? length d).
     intro; unfold C.valid; simpl; specialize (H5 (ur.[i])); rewrite length_amap, get_amap in H5 by assumption; unfold rho; rewrite H5; auto with smtcoq_core.
     intros; apply C.interp_true; auto with smtcoq_core.
     apply (foldi_ind _ (fun _ a => S.valid rho a)); [ apply leb_0 | | ]; auto with smtcoq_core; intros i a _ H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; unfold C.valid; simpl; specialize (H5 i); rewrite length_amap, get_amap in H5 by assumption; unfold rho; rewrite H5; auto with smtcoq_core.
@@ -733,7 +733,7 @@ Inductive step :=
   Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) :=
     negb (Lit.is_pos l) &&
     match t_form.[Lit.blit l] with
-      | Form.Fiff l1' l2' => (l1 == l1') && (l2 == l2')
+      | Form.Fiff l1' l2' => (l1 =? l1') && (l2 =? l2')
       | _ => false
     end &&
     let (nclauses,_,_) := c in
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index 3e403b3..78f7101 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -40,7 +40,7 @@ Section certif.
             | Atop (TO_store ti2 te2) fa j v2 =>
               if Typ.eqb ti1 ti2 &&
                  Typ.eqb te te1 && Typ.eqb te te2 &&
-                 (i == j) && (v == v2)
+                 (i =? j) && (v =? v2)
               then lres::nil
               else C._true
             | _ => C._true
@@ -57,7 +57,7 @@ Section certif.
   Definition store_of_me a b :=
     match get_atom b with
     | Atop (TO_store ti te) a' i _ =>
-      if (a' == a) then Some (ti, te, i) else None
+      if (a' =? a) then Some (ti, te, i) else None
     | _ => None
     end.
  
@@ -77,8 +77,8 @@ Section certif.
                 match store_of_me sa sa2, store_of_me sa2 sa with
                 | Some (ti3, te3, i1), None | None, Some (ti3, te3, i1) => 
                   if Typ.eqb ti ti3 && Typ.eqb te te3 &&
-                     (((i1 == i) && (j1 == j) && (j2 == j)) ||
-                      ((i1 == j) && (j1 == i) && (j2 == i))) then
+                     (((i1 =? i) && (j1 =? j) && (j2 =? j)) ||
+                      ((i1 =? j) && (j1 =? i) && (j2 =? i))) then
                     cl
                   else C._true
                 | _, _ => C._true
@@ -101,11 +101,11 @@ Section certif.
     | Abop (BO_select ti1 te1) a' d1, Abop (BO_select ti2 te2) b' d2 =>
       Typ.eqb ti ti1 && Typ.eqb ti ti2 &&
       Typ.eqb te te1 && Typ.eqb te te2 &&
-      (a == a') && (b == b') && (d1 == d2) &&
+      (a =? a') && (b =? b') && (d1 =? d2) &&
       match get_atom d1 with
       | Abop (BO_diffarray ti3 te3) a3 b3 =>
         Typ.eqb ti ti3 && Typ.eqb te te3 &&
-        (a3 == a) && (b3 == b)
+        (a3 =? a) && (b3 =? b)
       | _ => false
       end
     | _, _ => false
@@ -116,7 +116,7 @@ Section certif.
     if Lit.is_pos lres then
       match get_form (Lit.blit lres) with
       | For args =>
-        if PArray.length args == 2 then
+        if PArray.length args =? 2 then
           let l1 := args.[0] in
           let l2 := args.[1] in
           if Lit.is_pos l1 && negb (Lit.is_pos l2) then
@@ -213,7 +213,7 @@ Section certif.
       intros [ ] c1 c2 c3 Heq5.
       (* roweq *)
       - case_eq (Typ.eqb t0 t2 && Typ.eqb t t1 && 
-             Typ.eqb t t3 && (b2 == c2) && (a2 == c3)); simpl; intros Heq6; try (now apply C.interp_true).
+             Typ.eqb t t3 && (b2 =? c2) && (a2 =? c3)); simpl; intros Heq6; try (now apply C.interp_true).
 
         unfold C.valid. simpl. rewrite orb_false_r.
         unfold Lit.interp. rewrite Heq.
@@ -235,7 +235,7 @@ Section certif.
         generalize wt_t_atom. unfold Atom.wt. unfold is_true.
         rewrite aforallbi_spec;intros.
 
-        pose proof (H a). assert (a < PArray.length t_atom).
+        pose proof (H a). assert (a <? PArray.length t_atom).
         apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy.
         specialize (H0 H1). simpl in H0.
         rewrite Heq3 in H0. simpl in H0.
@@ -269,7 +269,7 @@ Section certif.
         specialize (Atom.Bval_inj2 t_i (Typ.Tbool) (Typ.i_eqb t_i t v_vala1 v_vala2) (v_vala)).
         intros. specialize (H5 Htia).
 
-        pose proof (H a1). assert (a1 < PArray.length t_atom).
+        pose proof (H a1). assert (a1 <? PArray.length t_atom).
         apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4. easy.
         specialize (H6 H7). simpl in H6.
         rewrite Heq4 in H6. simpl in H6.
@@ -279,7 +279,7 @@ Section certif.
         apply Typ.eqb_spec in H6b.
         apply Typ.eqb_spec in H6c.
 
-        pose proof (H b1). assert (b1 < PArray.length t_atom).
+        pose proof (H b1). assert (b1 <? PArray.length t_atom).
         apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq5. easy.
         specialize (H6 H8). simpl in H6.
         rewrite Heq5 in H6. simpl in H6.
@@ -442,13 +442,13 @@ Section certif.
         generalize wt_t_atom. unfold Atom.wt. unfold is_true.
         rewrite aforallbi_spec;intros.
 
-        assert (H15: b1 < PArray.length t_atom).
+        assert (H15: b1 <? PArray.length t_atom).
         apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq7. discriminate.
-        assert (H20: b2 < PArray.length t_atom).
+        assert (H20: b2 <? PArray.length t_atom).
         apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq8. discriminate.
-        assert (H9: b < PArray.length t_atom).
+        assert (H9: b <? PArray.length t_atom).
         apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. discriminate.
-        assert (H3: a < PArray.length t_atom).
+        assert (H3: a <? PArray.length t_atom).
         apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq5. discriminate.
 
 
@@ -594,13 +594,13 @@ Section certif.
           intro HT1. clear HT1.
           case_eq (t_atom .[ d1]); try discriminate.
           intros [ t5 t6 ] e1 e2 e3 Heq10 [[ti3 te3] i1].
-          case_eq (e1 == c1); try discriminate. intros Heq11c.
+          case_eq (e1 =? c1); try discriminate. intros Heq11c.
           intro HT.
           injection HT. intros. subst i1 te3 ti3. clear HT.
 
           case_eq (
               Typ.eqb t t5 && Typ.eqb v_typeb1' t6 &&
-                      ((e2 == a1) && (c2 == a2) && (d2 == a2) || (e2 == a2) && (c2 == a1) && (d2 == a1)));
+                      ((e2 =? a1) && (c2 =? a2) && (d2 =? a2) || (e2 =? a2) && (c2 =? a1) && (d2 =? a1)));
             simpl; intros Heq11; try (now apply C.interp_true).
 
           unfold C.valid. simpl. rewrite orb_false_r.
@@ -639,7 +639,7 @@ Section certif.
           unfold Bval in isif.
 
 
-          assert (H25: d1 < PArray.length t_atom).
+          assert (H25: d1 <? PArray.length t_atom).
           apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq10. discriminate.
           apply H2 in H25.
           rewrite Heq10 in H25.
@@ -750,13 +750,13 @@ Section certif.
         - unfold store_of_me.
           case_eq (t_atom .[ c1]); try discriminate.
           intros [ t5 t6 ] e1 e2 e3 Heq10 [[ti3 te3] i1].
-          case_eq (e1 == d1); try discriminate. intros Heq11d.
+          case_eq (e1 =? d1); try discriminate. intros Heq11d.
           intro HT.
           injection HT. intros E2 T6 T5 [ ]. subst i1 te3 ti3. clear HT.
 
           case_eq (
               Typ.eqb t t5 && Typ.eqb v_typeb1' t6 &&
-                      ((e2 == a1) && (c2 == a2) && (d2 == a2) || (e2 == a2) && (c2 == a1) && (d2 == a1)));
+                      ((e2 =? a1) && (c2 =? a2) && (d2 =? a2) || (e2 =? a2) && (c2 =? a1) && (d2 =? a1)));
             simpl; intros Heq11; try (now apply C.interp_true).
 
           unfold C.valid. simpl. rewrite orb_false_r.
@@ -796,7 +796,7 @@ Section certif.
           rewrite !Typ.cast_refl in isif.
           
 
-          assert (H25: c1 < PArray.length t_atom).
+          assert (H25: c1 <? PArray.length t_atom).
           apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq10. discriminate.
           apply H2 in H25.
           rewrite Heq10 in H25.
@@ -908,7 +908,7 @@ Section certif.
     case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
     case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true).
     intros a Heq2.
-    case_eq (length a == 2); [ intros Heq3 | intros Heq3; now apply C.interp_true].
+    case_eq (length a =? 2); [ intros Heq3 | intros Heq3; now apply C.interp_true].
     case_eq (Lit.is_pos (a .[ 0]) && negb (Lit.is_pos (a .[ 1])));
       [ intros Heq4 | intros Heq4; now apply C.interp_true].
     case_eq (t_form .[ Lit.blit (a .[0])]); try (intros; now apply C.interp_true).
@@ -935,8 +935,8 @@ Section certif.
     case_eq (Typ.eqb t0 t7 && Typ.eqb t1 t8);
       [ intros Heq14'| intro; rewrite !andb_false_r; simpl; now apply C.interp_true].
     simpl.
-    case_eq ((b1 == d1) && (b2 == e1) && (d2 == e2) && ((f1 == b1) && (f2 == b2))
-             || (b2 == d1) && (b1 == e1) && (d2 == e2) && ((f1 == b2) && (f2 == b1)));
+    case_eq ((b1 =? d1) && (b2 =? e1) && (d2 =? e2) && ((f1 =? b1) && (f2 =? b2))
+             || (b2 =? d1) && (b1 =? e1) && (d2 =? e2) && ((f1 =? b2) && (f2 =? b1)));
         [ intros Heq1314 | intro; now apply C.interp_true].
 
     unfold C.valid. simpl. rewrite orb_false_r.
@@ -999,7 +999,7 @@ Section certif.
     rewrite aforallbi_spec;intros.
 
     (* b *)
-    pose proof (H1 b). assert (b < PArray.length t_atom).
+    pose proof (H1 b). assert (b <? PArray.length t_atom).
     apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq7. easy.
     specialize (H2 H3). simpl in H2.
     rewrite Heq7 in H2. simpl in H2.
@@ -1035,7 +1035,7 @@ Section certif.
     intros. specialize (H7 Htib).
 
     (* c *)
-    pose proof (H1 c). assert (c < PArray.length t_atom).
+    pose proof (H1 c). assert (c <? PArray.length t_atom).
     apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy.
     specialize (H8 H9). simpl in H8.
     rewrite Heq9 in H8. simpl in H8.
@@ -1070,7 +1070,7 @@ Section certif.
     intros. specialize (H13 Htic).
 
     (* c1 *)
-    pose proof (H1 c1). assert (c1 < PArray.length t_atom).
+    pose proof (H1 c1). assert (c1 <? PArray.length t_atom).
     apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq11. easy.
     specialize (H14 H15). simpl in H14.
     rewrite Heq11 in H14. simpl in H14.
@@ -1106,7 +1106,7 @@ Section certif.
     intros. specialize (H18 Htic1').
 
     (* c2 *)
-    pose proof (H1 c2). assert (c2 < PArray.length t_atom).
+    pose proof (H1 c2). assert (c2 <? PArray.length t_atom).
     apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq12. easy.
     specialize (H19 H20). simpl in H19.
     rewrite Heq12 in H19. simpl in H19.
@@ -1143,7 +1143,7 @@ Section certif.
     intros. specialize (H23 Htic2').
 
     (* d2 *)
-    pose proof (H1 d2). assert (d2 < PArray.length t_atom).
+    pose proof (H1 d2). assert (d2 <? PArray.length t_atom).
     apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq14. easy.
     specialize (H24 H25). simpl in H24.
     rewrite Heq14 in H24. simpl in H24.
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index 261f660..dc8660c 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -668,7 +668,7 @@ Fixpoint mult_bool_step_k_h (a b: list bool) (c: bool) (k: Z) : list bool :=
 Local Open Scope int63_scope.
 
 Fixpoint top_k_bools (a: list bool) (k: int) : list bool :=
-  if (k == 0) then nil
+  if (k =? 0) then nil
   else match a with
          | nil => nil
          | ai :: a' => ai :: top_k_bools a' (k - 1)
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 24917a8..5c14bab 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -96,7 +96,7 @@ Section Checker.
           | Auop (UO_BVbitOf N p) a' =>
             (* TODO:
                Do not need to check [Nat.eqb l (N.to_nat N)] at every iteration *)
-            if (a == a')                     (* We bit blast the right bv *)
+            if (a =? a')                     (* We bit blast the right bv *)
                  && (Nat.eqb i p)            (* We consider bits after bits *)
                  && (Nat.eqb n (N.to_nat N)) (* The bv has indeed type BV n *)
             then check_bb a bs (S i) n
@@ -133,7 +133,7 @@ Section Checker.
   Fixpoint check_not (bs br : list _lit)  :=
     match bs, br with
     | nil, nil => true
-    | b::bs, r::br => (r == Lit.neg b) && check_not bs br
+    | b::bs, r::br => (r =? Lit.neg b) && check_not bs br
     | _, _ => false
     end.
 
@@ -146,7 +146,7 @@ Section Checker.
         | FbbT a bs, FbbT r br =>
           match get_atom r with
           | Auop (UO_BVnot N) a' =>
-            if (a == a') && check_not bs br &&
+            if (a =? a') && check_not bs br &&
               (N.of_nat (length bs) =? N)%N
             then lres::nil
             else C._true
@@ -174,25 +174,25 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
         match get_form (Lit.blit bres), bvop with
 
           | Fand args, BO_BVand n  =>
-            ((if PArray.length args == 2 then
+            ((if PArray.length args =? 2 then
                 let a1 := args.[0] in
                 let a2 := args.[1] in
-                ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1))
+                ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1))
               else false), BO_BVand (n-1))
 
           | For args, BO_BVor n  =>
-            ((if PArray.length args == 2 then
+            ((if PArray.length args =? 2 then
                 let a1 := args.[0] in
                 let a2 := args.[1] in
-                ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1))
+                ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1))
               else false), BO_BVor (n-1))
 
           | Fxor a1 a2, BO_BVxor n =>
-             (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)),
+             (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)),
              BO_BVxor (n-1))
 
           | Fiff a1 a2, (BO_eq (Typ.TBV n))  =>
-             (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)),
+             (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)),
              BO_eq (Typ.TBV n))
 
           | _, _ => (false, bvop)
@@ -218,21 +218,21 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
           match get_atom a with
 
           | Abop (BO_BVand n) a1' a2' =>
-            if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1')))
+            if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1')))
                  && (@check_symopp bs1 bs2 bsres (BO_BVand n))
                  && (N.of_nat (length bs1) =? n)%N
             then lres::nil
             else C._true
 
           | Abop (BO_BVor n) a1' a2' =>
-             if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1')))
+             if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1')))
                   && (check_symopp bs1 bs2 bsres  (BO_BVor n))
                   && (N.of_nat (length bs1) =? n)%N
              then lres::nil
              else C._true
 
           | Abop (BO_BVxor n) a1' a2' =>
-             if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1')))
+             if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1')))
                   && (check_symopp bs1 bs2 bsres  (BO_BVxor n))
                   && (N.of_nat (length bs1) =? n)%N
              then lres::nil
@@ -268,7 +268,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
                 let ires := 
                     match get_form (Lit.blit bres) with
                     | Fiff a1 a2  =>
-                      ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1))
+                      ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1))
                     | _ => false
                     end in
                 if ires then check_eq bs1 bs2 bsres
@@ -284,7 +284,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
           let ires := 
               match get_form (Lit.blit bres) with
               | Fiff a1 a2  =>
-                ((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1))
+                ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1))
               | _ => false
               end in
           if ires then check_eq bs1 bs2 bsres
@@ -306,7 +306,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
           | Fatom a, _ (* | _, Fatom a *) =>
             match get_atom a with
             | Abop (BO_eq (Typ.TBV n)) a1' a2' =>
-              if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1')))
+              if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1')))
                    && (check_eq bs1 bs2 [lbb])
                    && (N.of_nat (length bs1) =? n)%N
               then lres::nil
@@ -340,12 +340,12 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
   Fixpoint eq_carry_lit (carry : carry) (c : _lit) :=
     if Lit.is_pos c then
       match carry with
-        | Clit l => l == c
+        | Clit l => l =? c
 
         | Cand c1 c2  =>
           match get_form (Lit.blit c) with
           | Fand args =>
-            if PArray.length args == 2 then
+            if PArray.length args =? 2 then
               (eq_carry_lit c1 (args.[0]) && eq_carry_lit c2 (args.[1]))
               (* || (eq_carry_lit c1 (args.[1]) && eq_carry_lit c2 (args.[0])) *)
             else false
@@ -363,7 +363,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
         | Cor c1 c2  =>
           match get_form (Lit.blit c) with
           | For args =>
-            if PArray.length args == 2 then
+            if PArray.length args =? 2 then
               (eq_carry_lit c1 (args.[0]) && eq_carry_lit c2 (args.[1]))
                 (* || (eq_carry_lit c1 (args.[1]) && eq_carry_lit c2 (args.[0])) *)
             else false
@@ -381,7 +381,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
     else
       (* c can be negative only when it is literal false *)
       match carry with
-        | Clit l => l == c
+        | Clit l => l =? c
         | _ => false
       end.
 
@@ -400,7 +400,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
                   (* This is the way LFSC computes carries *)
                   let carry' := Cor (Cand (Clit b1) (Clit b2))
                                    (Cand (Cxor (Clit b1) (Clit b2)) carry) in
-                  (((a1 == b1) && (a2 == b2)) || ((a1 == b2) && (a2 == b1)))
+                  (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)))
                     && eq_carry_lit carry c
                     && check_add bs1 bs2 bsres carry'
                 | _ => false
@@ -422,7 +422,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
               match get_atom a with
 
                 | Abop (BO_BVadd n) a1' a2' =>
-                  if (((a1 == a1') && (a2 == a2')) || ((a1 == a2') && (a2 == a1')))
+                  if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1')))
                        && (check_add bs1 bs2 bsres (Clit Lit._false))
                        && (N.of_nat (length bs1) =? n)%N
                   then lres::nil
@@ -458,7 +458,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
         | FbbT a bs, FbbT r br =>
           match get_atom r with
           | Auop (UO_BVneg n) a' =>
-            if (a == a') && check_neg bs br &&
+            if (a =? a') && check_neg bs br &&
                (N.of_nat (length bs) =? n)%N
             then lres::nil
             else C._true
@@ -545,7 +545,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
               match get_atom a with
 
                 | Abop (BO_BVmult n) a1' a2' =>
-                  if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) )
+                  if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) )
                        && (check_mult bs1 bs2 bsres)
                        && (N.of_nat (length bs1) =? n)%N
                   then lres::nil
@@ -590,7 +590,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
           | Fatom a, _ (* | _, Fatom a *) =>
             match get_atom a with
             | Abop (BO_BVult n) a1' a2' =>
-              if ((a1 == a1') && (a2 == a2'))
+              if ((a1 =? a1') && (a2 =? a2'))
                    && (check_ult bs1 bs2 lbb)
                    && (N.of_nat (length bs1) =? n)%N
                    && (N.of_nat (length bs2) =? n)%N
@@ -636,7 +636,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
           | Fatom a, _ (* | _, Fatom a *) =>
             match get_atom a with
             | Abop (BO_BVslt n) a1' a2' =>
-              if ((a1 == a1') && (a2 == a2'))
+              if ((a1 =? a1') && (a2 =? a2'))
                    && (check_slt bs1 bs2 lbb)
                    && (N.of_nat (length bs1) =? n)%N
                    && (N.of_nat (length bs2) =? n)%N
@@ -691,7 +691,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
               match get_atom a with
 
                 | Abop (BO_BVconcat n m) a1' a2' =>
-                  if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) )
+                  if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) )
                        && (check_concat bs1 bs2 bsres)
                        && (N.of_nat (length bs1) =? n)%N
                        && (N.of_nat (length bs2) =? m)%N
@@ -771,7 +771,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
        else false.
 
   Definition check_extract3 (bs bsres: list _lit) (i j: N) : bool :=
-    forallb2 (fun l1 l2 => l1 == l2) (extract_lit bs (nat_of_N i) (nat_of_N j)) bsres.
+    forallb2 (fun l1 l2 => l1 =? l2) (extract_lit bs (nat_of_N i) (nat_of_N j)) bsres.
 
 
   (** Checker for bitvector extraction *)
@@ -783,7 +783,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
           | O      =>
             match j, bsres with
             | O, nil => true
-            | S j', b :: bsres' => (bx == b) && check_extract2 x' bsres' i j'
+            | S j', b :: bsres' => (bx =? b) && check_extract2 x' bsres' i j'
             | _, _ => false
             end
           | S i'   => 
@@ -804,7 +804,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
               match get_atom a with
 
                 | Auop (UO_BVextr i n0 n1) a1' =>
-                  if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) )
+                  if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) )
                        && (check_extract bs bsres i (n0 + i))
                        && (N.of_nat (length bs) =? n1)%N
                        && (N.leb (n0 + i) n1)
@@ -847,7 +847,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
               match get_atom a with
 
                 | Auop (UO_BVzextn n i) a1' =>
-                  if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) )
+                  if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) )
                        && (check_zextend bs bsres i)
                        && (N.of_nat (length bs) =? n)%N
                   then lres::nil
@@ -889,7 +889,7 @@ Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop)  :=
               match get_atom a with
 
                 | Auop (UO_BVsextn n i) a1' =>
-                  if ((a1 == a1') (* || ((a1 == a2') && (a2 == a1')) *) )
+                  if ((a1 =? a1') (* || ((a1 =? a2') && (a2 =? a1')) *) )
                        && (check_sextend bs bsres i)
                        && (N.of_nat (length bs) =? n)%N
                   then lres::nil
@@ -938,7 +938,7 @@ Definition shl_lit_be (a: list _lit) (b: list bool): list _lit :=
                 | Abop (BO_BVshl n) a1' a2' =>
                   match (get_atom a2) with
                     |  (Acop (CO_BV bv2 n2)) =>                
-                      if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) )
+                      if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) )
                          && check_shl bs1 bv2 bsres
                          && (N.of_nat (length bs1) =? n)%N
                          && (N.of_nat (length bv2) =? n)%N
@@ -989,7 +989,7 @@ Definition shr_lit_be (a: list _lit) (b: list bool): list _lit :=
                 | Abop (BO_BVshr n) a1' a2' =>
                   match (get_atom a2) with
                     |  (Acop (CO_BV bv2 n2)) =>                
-                      if (((a1 == a1') && (a2 == a2')) (* || ((a1 == a2') && (a2 == a1')) *) )
+                      if (((a1 =? a1') && (a2 =? a2')) (* || ((a1 =? a2') && (a2 =? a1')) *) )
                          && check_shr bs1 bv2 bsres
                          && (N.of_nat (length bs1) =? n)%N
                          && (N.of_nat (length bv2) =? n)%N
@@ -1211,7 +1211,7 @@ Proof.
 
   (* a *)
   pose proof (H a).
-  assert (H1: a < PArray.length t_atom).
+  assert (H1: a <? PArray.length t_atom).
   { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq4, Heq5. easy. }
   specialize (@H0 H1). rewrite Heq4 in H0. simpl in H0.
   unfold get_type' in H0. unfold v_type in H0.
@@ -1229,7 +1229,7 @@ Proof.
 
   (* b *)
   pose proof (H b).
-  assert (H4: b < PArray.length t_atom).
+  assert (H4: b <? PArray.length t_atom).
   { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6, Heq7. easy. }
   specialize (@H2 H4). rewrite Heq6 in H2. simpl in H2.
   unfold get_type' in H2. unfold v_type in H2.
@@ -1247,7 +1247,7 @@ Proof.
 
   (* f *)
   pose proof (H f).
-  assert (H7: f < PArray.length t_atom).
+  assert (H7: f <? PArray.length t_atom).
   { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq3. easy. }
   specialize (@H5 H7). rewrite Heq3 in H5. simpl in H5.
   unfold get_type' in H5. unfold v_type in H5.
@@ -1316,7 +1316,7 @@ Proof. intros a bs.
          case_eq u; try (intro Heq'; rewrite Heq' in H0; now contradict H0).
 
          intros. rewrite H2 in H0.
-         case_eq ((a == i2) && Nat.eqb i n1 && Nat.eqb n (N.to_nat n0)). intros Hif.
+         case_eq ((a =? i2) && Nat.eqb i n1 && Nat.eqb n (N.to_nat n0)). intros Hif.
          rewrite Hif in H0.
          do 2 rewrite andb_true_iff in Hif. destruct Hif as ((Hif0 & Hif1) & Hif2).
          specialize (@IHys a (S i) n).
@@ -1352,7 +1352,7 @@ Proof. intros a bs.
 
          generalize wt_t_atom. unfold Atom.wt. unfold is_true.
          rewrite aforallbi_spec;intros.
-         assert (i1 < PArray.length t_atom).
+         assert (i1 <? PArray.length t_atom).
          {
            apply PArray.get_not_default_lt.
            rewrite Heq2. now rewrite def_t_atom.
@@ -1785,7 +1785,7 @@ Proof.
   intros u a'.
   case_eq u; try (intros; now apply C.interp_true).
   intros n Huot Hr.
-  case_eq ((a == a')
+  case_eq ((a =? a')
              && check_not bs br
              && (N.of_nat (Datatypes.length bs) =? n)%N);
     try (intros; now apply C.interp_true).
@@ -1812,7 +1812,7 @@ Proof.
   rewrite aforallbi_spec;intros.
 
   pose proof (H r). 
-  assert (r < PArray.length t_atom).
+  assert (r <? PArray.length t_atom).
   {
     apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Hr. easy.
   }
@@ -1914,7 +1914,7 @@ Qed.
 Lemma eq_head: forall {A: Type} a b (l: list A), (a :: l) = (b :: l) <-> a = b.
 Proof. intros A a b l; split; [intros H; inversion H|intros ->]; auto. Qed.
 
-Lemma eqb_spec : forall x y, (x == y) = true <-> x = y.
+Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y.
 Proof.
  split;auto using eqb_correct, eqb_complete.
 Qed.
@@ -1937,9 +1937,9 @@ Proof. intros.
        simpl in H. 
        case (Lit.is_pos ibsres) in H.
        case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy).
-       case (PArray.length a == 2) in H.
-       case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)
-         || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H.
+       case (PArray.length a =? 2) in H.
+       case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)
+         || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H.
        exact H.
        now contradict H.
        now contradict H.
@@ -1947,9 +1947,9 @@ Proof. intros.
        unfold check_symopp in H.
        case (Lit.is_pos ibsres) in H.
        case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy).
-       case (PArray.length a == 2) in H.
-       case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)
-        || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H.
+       case (PArray.length a =? 2) in H.
+       case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)
+        || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H.
        apply H.
        now contradict H.
        now contradict H.
@@ -1964,9 +1964,9 @@ Proof. intros.
        simpl in H. 
        case (Lit.is_pos ibsres) in H.
        case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy).
-       case (PArray.length a == 2) in H.
-       case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)
-         || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H.
+       case (PArray.length a =? 2) in H.
+       case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)
+         || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H.
        exact H.
        now contradict H.
        now contradict H.
@@ -1974,9 +1974,9 @@ Proof. intros.
        unfold check_symopp in H.
        case (Lit.is_pos ibsres) in H.
        case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy).
-       case (PArray.length a == 2) in H.
-       case ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)
-        || (a .[ 0] == ibs2) && (a .[ 1] == ibs1)) in H.
+       case (PArray.length a =? 2) in H.
+       case ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)
+        || (a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)) in H.
        apply H.
        now contradict H.
        now contradict H.
@@ -1991,14 +1991,14 @@ Proof. intros.
        simpl in H. 
        case (Lit.is_pos ibsres) in H.
        case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy).
-       case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H.
+       case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H.
        exact H.
        now contradict H.
        now contradict H.
        unfold check_symopp in H.
        case (Lit.is_pos ibsres) in H.
        case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy).
-       case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H.
+       case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H.
        apply H.
        now contradict H.
        now contradict H.
@@ -2041,20 +2041,20 @@ Proof. intro bs1.
                intros. rewrite H2 in H1. simpl.
                rewrite afold_left_and.
 
-                case_eq (PArray.length a == 2). intros. rewrite H3 in H1.
+                case_eq (PArray.length a =? 2). intros. rewrite H3 in H1.
                 rewrite eqb_spec in H3.
                 apply to_list_two in H3.
              (*   apply length_to_list in H4. *)
                 unfold forallb.
                 rewrite H3.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold Lit.interp.
                 rewrite Heq1, Heq2.
                 unfold Var.interp. now rewrite andb_true_r.
                 intros. rewrite H4 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)).
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)).
                 intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6.
@@ -2100,19 +2100,19 @@ Proof. intro bs1.
                intros. rewrite H2 in H1. simpl.
                rewrite afold_left_and.
 
-                case_eq (PArray.length a == 2). intros. rewrite H3 in H1.
+                case_eq (PArray.length a =? 2). intros. rewrite H3 in H1.
                 rewrite eqb_spec in H3.
                 apply to_list_two in H3.
                 unfold forallb.
                 rewrite H3.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold Lit.interp.
                 rewrite Heq1, Heq2.
                 unfold Var.interp. now rewrite andb_true_r.
                 intros H4. rewrite H4 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5.
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H6 & H7).
                 rewrite eqb_spec in H6, H7.
                 rewrite H6, H7. rewrite andb_true_r.
@@ -2164,19 +2164,19 @@ Proof. intro bs1.
                intros. rewrite H2 in H1. simpl.
                rewrite afold_left_and.
 
-                case_eq (PArray.length a == 2). intros. rewrite H3 in H1.
+                case_eq (PArray.length a =? 2). intros. rewrite H3 in H1.
                 rewrite eqb_spec in H3.
                 apply to_list_two in H3.
                 unfold forallb.
                 rewrite H3.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold Lit.interp.
                 rewrite Heq1, Heq2.
                 unfold Var.interp. now rewrite andb_true_r.
                 intros. rewrite H4 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5.
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H6 & H7).
                 rewrite eqb_spec in H6, H7.
                 rewrite H6, H7. rewrite andb_true_r.
@@ -2226,20 +2226,20 @@ Proof. intro bs1.
                intros. rewrite H3 in H1. simpl.
                rewrite afold_left_and.
 
-               case_eq (PArray.length a == 2). intros H5.
+               case_eq (PArray.length a =? 2). intros H5.
                 rewrite H5 in H1.
                 rewrite eqb_spec in H5.
                 apply to_list_two in H5.
                 unfold forallb.
                 rewrite H5.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H6.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H6.
                 rewrite andb_true_iff in H6. destruct H6 as (H6 & H7).
                 rewrite eqb_spec in H6, H7. rewrite H6, H7.
                 unfold Lit.interp.
                 rewrite Heq1, H2.
                 unfold Var.interp. now rewrite andb_true_r.
                 intros H6. rewrite H6 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H7.
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H7.
                 rewrite andb_true_iff in H7. destruct H7 as (H7 & H8).
                 rewrite eqb_spec in H7, H8.
                 rewrite H7, H8. rewrite andb_true_r.
@@ -2310,12 +2310,12 @@ Proof. intro bs1.
                intros. rewrite H2 in H1. simpl.
                rewrite afold_left_or.
 
-                case_eq (PArray.length a == 2). intros. rewrite H3 in H1.
+                case_eq (PArray.length a =? 2). intros. rewrite H3 in H1.
                 rewrite eqb_spec in H3.
                 apply to_list_two in H3.
                 unfold forallb.
                 rewrite H3.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold C.interp. unfold existsb. rewrite orb_false_r.
@@ -2325,7 +2325,7 @@ Proof. intro bs1.
                 now unfold Var.interp.
 
                 intros. rewrite H4 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)).
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)).
                 intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6.
@@ -2369,21 +2369,21 @@ Proof. intro bs1.
                intros. rewrite H2 in H1. simpl.
                rewrite afold_left_or.
 
-                case_eq (PArray.length a == 2). intros. rewrite H3 in H1.
+                case_eq (PArray.length a =? 2). intros. rewrite H3 in H1.
                 rewrite eqb_spec in H3.
                 apply to_list_two in H3.
                 unfold C.interp.
                 unfold existsb.
 
                 rewrite H3.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold Lit.interp.
                 rewrite Heq1, Heq2.
                 unfold Var.interp. now rewrite orb_false_r.
                 intros H4. rewrite H4 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5.
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H6 & H7).
                 rewrite eqb_spec in H6, H7.
                 rewrite H6, H7. rewrite orb_false_r.
@@ -2433,12 +2433,12 @@ Proof. intro bs1.
                intros. rewrite H2 in H1. simpl.
                rewrite afold_left_or.
 
-                case_eq (PArray.length a == 2). intros. rewrite H3 in H1.
+                case_eq (PArray.length a =? 2). intros. rewrite H3 in H1.
                 rewrite eqb_spec in H3.
                 apply to_list_two in H3.
                 unfold forallb.
                 rewrite H3.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H5.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold C.interp, existsb.
@@ -2446,7 +2446,7 @@ Proof. intro bs1.
                 rewrite Heq1, Heq2.
                 unfold Var.interp. now rewrite orb_false_r.
                 intros. rewrite H4 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H5.
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H6 & H7).
                 rewrite eqb_spec in H6, H7.
                 rewrite H6, H7. rewrite orb_false_r.
@@ -2494,20 +2494,20 @@ Proof. intro bs1.
                intros. rewrite H3 in H1. simpl.
                rewrite afold_left_or.
 
-               case_eq (PArray.length a == 2). intros H5.
+               case_eq (PArray.length a =? 2). intros H5.
                 rewrite H5 in H1.
                 rewrite eqb_spec in H5.
                 apply to_list_two in H5.
                 unfold forallb.
                 rewrite H5.
-                case_eq ((a .[ 0] == ibs1) && (a .[ 1] == ibs2)). intros H6.
+                case_eq ((a .[ 0] =? ibs1) && (a .[ 1] =? ibs2)). intros H6.
                 rewrite andb_true_iff in H6. destruct H6 as (H6 & H7).
                 rewrite eqb_spec in H6, H7. rewrite H6, H7.
                 unfold C.interp, Lit.interp, existsb.
                 rewrite Heq1, H2.
                 unfold Var.interp. now rewrite orb_false_r.
                 intros H6. rewrite H6 in H1. simpl in *.
-                case_eq ((a .[ 0] == ibs2) && (a .[ 1] == ibs1)). intros H7.
+                case_eq ((a .[ 0] =? ibs2) && (a .[ 1] =? ibs1)). intros H7.
                 rewrite andb_true_iff in H7. destruct H7 as (H7 & H8).
                 rewrite eqb_spec in H7, H8.
                 rewrite H7, H8. rewrite orb_false_r.
@@ -2576,7 +2576,7 @@ Proof. intro bs1.
                try (intros a Heq; rewrite Heq in H1; now contradict H1).
                try (intros i Heq; rewrite Heq in H1; now contradict H1).
                intros. rewrite H2 in H1. simpl.
-                case_eq ((i == ibs1) && (i0 == ibs2)). intros H5.
+                case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
 
@@ -2585,7 +2585,7 @@ Proof. intro bs1.
                 now unfold Var.interp.
 
                 intros H4. rewrite H4 in H1. simpl in *.
-                case_eq ((i == ibs2) && (i0 == ibs1)).
+                case_eq ((i =? ibs2) && (i0 =? ibs1)).
                 intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6.
@@ -2629,14 +2629,14 @@ Proof. intro bs1.
                try (intros a Heq; rewrite Heq in H1; now contradict H1).
 
                intros. rewrite H2 in H1. simpl.
-                case_eq ((i == ibs1) && (i0 == ibs2)). intros H5.
+                case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold Lit.interp.
                 rewrite Heq1, Heq2.
                 now unfold Var.interp.
                 intros H4. rewrite Heq0, H4 in H1. simpl in *.
-                case_eq ((i == ibs2) && (i0 == ibs1)). intros H5.
+                case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H6 & H7).
                 rewrite eqb_spec in H6, H7.
                 rewrite H6, H7.
@@ -2686,14 +2686,14 @@ Proof. intro bs1.
 
                intros. rewrite H2 in H1. simpl.
 
-                case_eq ((i == ibs1) && (i0 == ibs2)). intros H5.
+                case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold Lit.interp.
                 rewrite Heq1, Heq2.
                 now unfold Var.interp.
                 intros H4. rewrite Heq0, H4 in H1. simpl in *.
-                case_eq ((i == ibs2) && (i0 == ibs1)). intros H5.
+                case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H6 & H7).
                 rewrite eqb_spec in H6, H7.
                 rewrite H6, H7.
@@ -2740,14 +2740,14 @@ Proof. intro bs1.
                try (intros a Heq; rewrite Heq in H1; now contradict H1).
 
                intros. rewrite H2 in H1. simpl.
-                case_eq ((i == ibs1) && (i0 == ibs2)). intros H5.
+                case_eq ((i =? ibs1) && (i0 =? ibs2)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H5 & H6).
                 rewrite eqb_spec in H5, H6. rewrite H5, H6.
                 unfold Lit.interp.
                 rewrite Heq1, Heq2.
                 now unfold Var.interp.
                 intros H4. rewrite Heq0, H4 in H1. simpl in *.
-                case_eq ((i == ibs2) && (i0 == ibs1)). intros H5.
+                case_eq ((i =? ibs2) && (i0 =? ibs1)). intros H5.
                 rewrite andb_true_iff in H5. destruct H5 as (H6 & H7).
                 rewrite eqb_spec in H6, H7.
                 rewrite H6, H7.
@@ -2796,8 +2796,8 @@ Proof.
   simpl in H.
   case (Lit.is_pos r) in H.
   case (t_form .[ Lit.blit r]) in H; try easy.
-  case (PArray.length a == 2) in H; try easy.
-  case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy.
+  case (PArray.length a =? 2) in H; try easy.
+  case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy.
   specialize (IHrbsres bs1 bs2 (N - 1)%N H).
   simpl.
   simpl in n.
@@ -2834,8 +2834,8 @@ Proof.
   simpl in H.
   case (Lit.is_pos r) in H.
   case (t_form .[ Lit.blit r]) in H; try easy.
-  case (PArray.length a == 2) in H; try easy.
-  case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy.
+  case (PArray.length a =? 2) in H; try easy.
+  case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy.
   specialize (IHrbsres bs1 bs2 (N - 1)%N H).
   simpl.
   simpl in n.
@@ -2871,8 +2871,8 @@ Proof. intros bs1 bs2 bsres.
              now contradict H.
              case (Lit.is_pos xbsres) in *.
              case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H.
-             case (PArray.length a == 2) in *.
-             case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in *.
+             case (PArray.length a =? 2) in *.
+             case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in *.
              specialize (IHbsres bs1 bs2 (n-1)%nat).
              simpl in H0.
              assert (length bs1 = (n-1)%nat).
@@ -2924,8 +2924,8 @@ Proof.
   simpl in H.
   case (Lit.is_pos r) in H.
   case (t_form .[ Lit.blit r]) in H; try easy.
-  case (PArray.length a == 2) in H; try easy.
-  case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy.
+  case (PArray.length a =? 2) in H; try easy.
+  case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy.
   specialize (IHrbsres bs1 bs2 (N - 1)%N H).
   simpl.
   simpl in n.
@@ -2961,8 +2961,8 @@ Proof.
   simpl in H.
   case (Lit.is_pos r) in H.
   case (t_form .[ Lit.blit r]) in H; try easy.
-  case (PArray.length a == 2) in H; try easy.
-  case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in H; try easy.
+  case (PArray.length a =? 2) in H; try easy.
+  case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in H; try easy.
   specialize (IHrbsres bs1 bs2 (N - 1)%N H).
   simpl.
   simpl in n.
@@ -2998,8 +2998,8 @@ Proof. intros bs1 bs2 bsres.
              now contradict H.
              case (Lit.is_pos xbsres) in *.
              case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H.
-             case (PArray.length a == 2) in *.
-             case ((a .[ 0] == i) && (a .[ 1] == i0) || (a .[ 0] == i0) && (a .[ 1] == i)) in *.
+             case (PArray.length a =? 2) in *.
+             case ((a .[ 0] =? i) && (a .[ 1] =? i0) || (a .[ 0] =? i0) && (a .[ 1] =? i)) in *.
              specialize (IHbsres bs1 bs2 (n-1)%nat).
              simpl in H0.
              assert (length bs1 = (n-1)%nat).
@@ -3051,7 +3051,7 @@ Proof.
   simpl in H.
   case (Lit.is_pos r) in H.
   case (t_form .[ Lit.blit r]) in H; try easy.
-  case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in H; try easy.
+  case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in H; try easy.
   specialize (IHrbsres bs1 bs2 (N - 1)%N H).
   simpl.
   simpl in n.
@@ -3088,7 +3088,7 @@ Proof.
   simpl in H.
   case (Lit.is_pos r) in H.
   case (t_form .[ Lit.blit r]) in H; try easy.
-  case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in H; try easy.
+  case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in H; try easy.
   specialize (IHrbsres bs1 bs2 (N - 1)%N H).
   simpl.
   simpl in n.
@@ -3124,7 +3124,7 @@ Proof. intros bs1 bs2 bsres.
              now contradict H.
              case (Lit.is_pos xbsres) in *.
              case (t_form .[ Lit.blit xbsres] ) in *; try now contradict H.
-             case ((i1 == i) && (i2 == i0) || (i1 == i0) && (i2 == i)) in *.
+             case ((i1 =? i) && (i2 =? i0) || (i1 =? i0) && (i2 =? i)) in *.
              specialize (IHbsres bs1 bs2 (n-1)%nat).
              simpl in H0.
              assert (length bs1 = (n-1)%nat).
@@ -3204,7 +3204,7 @@ Proof.
       intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9;
         try (intros; now apply C.interp_true).
       (* BVand *)
-      - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1'));
+      - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1'));
           simpl; intros Heq10; try (now apply C.interp_true).
 
         case_eq (
@@ -3227,7 +3227,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } 
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -3537,7 +3537,7 @@ Proof.
         exact Heq11.
 
       (* BVor *)
-      - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); 
+      - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); 
            simpl; intros Heq10; try (now apply C.interp_true).
 
         case_eq (
@@ -3560,7 +3560,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -3869,7 +3869,7 @@ Proof.
         exact Heq11.
 
         (** BVxor **)
-        - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); 
+        - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); 
             simpl; intros Heq10; try (now apply C.interp_true).
 
         case_eq (
@@ -3892,7 +3892,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a).
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -4210,7 +4210,7 @@ Proof. intros.
        simpl in H. 
        case (Lit.is_pos ibsres) in H.
        case (t_form .[ Lit.blit ibsres]) in H; try (contradict H; easy).
-       case ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)) in H.
+       case ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)) in H.
        exact H.
        now contradict H.
        now contradict H.
@@ -4228,7 +4228,7 @@ Proof. intros.
        case_eq (t_form .[ Lit.blit ibsres]); intros; rewrite H1 in H; try (now contradict H).
        specialize (@rho_interp ( Lit.blit ibsres)).
        rewrite H1 in rho_interp. simpl in rho_interp.
-       case_eq ((i == ibs1) && (i0 == ibs2) || (i == ibs2) && (i0 == ibs1)).
+       case_eq ((i =? ibs1) && (i0 =? ibs2) || (i =? ibs2) && (i0 =? ibs1)).
        intros. rewrite orb_true_iff in H2. destruct H2.
        rewrite andb_true_iff in H2. destruct H2. rewrite eqb_spec in H2, H3.
        rewrite H2, H3 in rho_interp.
@@ -4320,7 +4320,7 @@ Proof. intro bs1.
            (*++*) rename i into arg1; rename i0 into arg2.
               unfold Lit.interp at 1, Var.interp at 1.
               rewrite Hposr1, Hi. repeat (rewrite andb_true_r).
-              case_eq ((arg1 == x1) && (arg2 == x2) || (arg1 == x2) && (arg2 == x1)).
+              case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)).
               (* ** *) intros Hif.
                  rewrite orb_true_iff in Hif.
                  repeat (rewrite andb_true_iff in Hif).
@@ -4351,7 +4351,7 @@ Proof. intro bs1.
               unfold Lit.interp at 1, Var.interp at 1.
               rewrite Hposa1. rewrite Heqx1x2.
 
-              case_eq ((arg1 == x1) && (arg2 == x2) || (arg1 == x2) && (arg2 == x1)).
+              case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)).
               (* ** *) intros Hif.
                  rewrite Hif in Hcheck.
                  apply (@IHbs1 _ _ Hlen') in Hcheck.
@@ -4375,11 +4375,11 @@ Proof. intro bs1.
            generalize (rho_interp (Lit.blit r1)); rewrite Hform_r1; simpl;
            intro Hi.
           (* ++ *) contradict Hcheck. simpl.
-              case ((i0 == x1) && (i1 == x2) || (i0 == x2) && (i1 == x1)); easy.
+              case ((i0 =? x1) && (i1 =? x2) || (i0 =? x2) && (i1 =? x1)); easy.
           (* ++ *) rename i0 into x1', i1 into x2', i2 into arg1, i3 into arg2.
               unfold Lit.interp at 1, Var.interp at 1.
               rewrite Hposr1, Hi.
-              case_eq ((arg1 == x1) && (arg2 == x2) || (arg1 == x2) && (arg2 == x1)).
+              case_eq ((arg1 =? x1) && (arg2 =? x2) || (arg1 =? x2) && (arg2 =? x1)).
              (* ** *) intros Hif. rewrite Hif in Hcheck.
                  apply (@IHbs1 _ _ Hlen') in Hcheck.
                  simpl in Hcheck. rewrite Hcheck.
@@ -4424,7 +4424,7 @@ Proof.
       case (Lit.is_pos i2); try easy.
       case (t_form .[ Lit.blit i2]); try easy.
       intros i3 i4.
-      case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)).
+      case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)).
       apply IHbs1.
       easy.
       intros _ _ i2 l0 a0.
@@ -4433,7 +4433,7 @@ Proof.
       case (Lit.is_pos i1); try easy.
       case (t_form .[ Lit.blit i1]); try easy.
       intros i3 i4.
-      case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)).
+      case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)).
       apply IHbs1.
       easy.
       intros i2 l0 a0.
@@ -4442,7 +4442,7 @@ Proof.
       case (Lit.is_pos i9); try easy.
       case (t_form .[ Lit.blit i9]); try easy.
       intros i3 i4.
-      case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)).
+      case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)).
       apply IHbs1.
       easy.
       intros _ _ i2 l0 a0.
@@ -4451,7 +4451,7 @@ Proof.
       case (Lit.is_pos i9); try easy.
       case (t_form .[ Lit.blit i9]); try easy.
       intros i3 i4.
-      case ((i3 == a) && (i4 == i) || (i3 == i) && (i4 == a)).
+      case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)).
       apply IHbs1.
       easy.
       case bs1; try easy; case bs2; easy.
@@ -4462,10 +4462,10 @@ Proof.
       simpl. easy.
 
       intros i0 l i1 i2.
-      case ((i1 == a) && (i2 == i) || (i1 == i) && (i2 == a)); easy.
+      case ((i1 =? a) && (i2 =? i) || (i1 =? i) && (i2 =? a)); easy.
       simpl.
       intros _ l i1 i2.
-      case ((i1 == a) && (i2 == i) || (i1 == i) && (i2 == a)); easy.
+      case ((i1 =? a) && (i2 =? i) || (i1 =? i) && (i2 =? a)); easy.
       easy.
       case bs1 in *; try easy; case bs2; easy.
       case bs1 in *; try easy; case bs2; easy.
@@ -4473,13 +4473,13 @@ Proof.
       case bs1 in *; try easy; case bs2; try easy.
       case (Lit.is_pos r); try easy.
       case (t_form .[ Lit.blit r]); try easy.
-      simpl. intros x y. case ((x == a) && (y == i) || (x == i) && (y == a)); easy.
+      simpl. intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)); easy.
       case (Lit.is_pos r); try easy.
       case (t_form .[ Lit.blit r]); try easy.
-      simpl. intros x y. case ((x == a) && (y == i) || (x == i) && (y == a)); easy.
+      simpl. intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)); easy.
       case (Lit.is_pos r); try easy.
       case (t_form .[ Lit.blit r]); try easy.
-      intros x y. case ((x == a) && (y == i) || (x == i) && (y == a)).
+      intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)).
       intros x2 rbs2 xr rbrs.
       apply IHbs1. easy.
 Qed.
@@ -4503,7 +4503,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres).
           try (intros; now apply C.interp_true).
 
        intros a1' a2' Heq9.
-       case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1')); 
+       case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); 
          simpl; intros Heq15; try (now apply C.interp_true).
 
        case_eq (check_eq bs1 bs2 [bsres] &&
@@ -4520,7 +4520,7 @@ Lemma valid_check_bbEq pos1 pos2 lres : C.valid rho (check_bbEq pos1 pos2 lres).
        rewrite aforallbi_spec;intros.
 
        pose proof (H a3).
-       assert (a3 < PArray.length t_atom).
+       assert (a3 <? PArray.length t_atom).
        { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
        specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
        rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -4887,7 +4887,7 @@ Proof. intro c.
     case_eq ( Lit.is_pos i). intros Hip0.
     rewrite Hip0 in H.
     case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H.
-    case_eq (PArray.length a == 2). intros Hl. rewrite Hl in H.
+    case_eq (PArray.length a =? 2). intros Hl. rewrite Hl in H.
     (* rewrite orb_true_iff in H; do 2 *) rewrite andb_true_iff in H.
 
     specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp.
@@ -4935,7 +4935,7 @@ Proof. intro c.
     case_eq ( Lit.is_pos i). intros Hip0.
     rewrite Hip0 in H.
     case_eq (t_form .[ Lit.blit i]); intros; rewrite H2 in H; try now contradict H.
-    case_eq (PArray.length a == 2). intros Hl. rewrite Hl in H.
+    case_eq (PArray.length a =? 2). intros Hl. rewrite Hl in H.
     (* rewrite orb_true_iff in H; do 2 *) rewrite andb_true_iff in H.
 
     specialize (@rho_interp ( Lit.blit i)). rewrite H2 in rho_interp.
@@ -5158,7 +5158,7 @@ Proof.
          try (intros; now apply C.interp_true).
 
        intros a1' a2' Heq9.
-         case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq15; try (now apply C.interp_true).
+         case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq15; try (now apply C.interp_true).
 
        case_eq (check_ult bs1 bs2 bsres &&
           (N.of_nat (Datatypes.length bs1) =? N)%N &&
@@ -5176,7 +5176,7 @@ Proof.
        rewrite aforallbi_spec;intros.
 
        pose proof (H a3).
-       assert (a3 < PArray.length t_atom).
+       assert (a3 <? PArray.length t_atom).
        { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
        specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
        rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -5383,7 +5383,7 @@ Proof.
        intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; 
           try (intros; now apply C.interp_true).
 
-       case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq15; try (now apply C.interp_true).
+       case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq15; try (now apply C.interp_true).
 
        case_eq (check_slt bs1 bs2 bsres &&
           (N.of_nat (Datatypes.length bs1) =? N)%N &&
@@ -5401,7 +5401,7 @@ Proof.
        rewrite aforallbi_spec;intros.
 
        pose proof (H a3).
-       assert (a3 < PArray.length t_atom).
+       assert (a3 <? PArray.length t_atom).
        { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
        specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
        rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -5795,7 +5795,7 @@ Proof.
         try (intros; now apply C.interp_true).
 
       (* BVadd *)
-      - case_eq ((a1 == a1') && (a2 == a2') || (a1 == a2') && (a2 == a1'));
+      - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1'));
             simpl; intros Heq10; try (now apply C.interp_true).
         case_eq (
                  check_add bs1 bs2 bsres (Clit Lit._false) &&
@@ -5813,7 +5813,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -6246,7 +6246,7 @@ Proof.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
       intros [ | | | | | | | | | | ] a1' Heq9; try now apply C.interp_true.
 
-      case_eq ((a1 == a1') && check_neg bs1 bsres &&
+      case_eq ((a1 =? a1') && check_neg bs1 bsres &&
       (N.of_nat (Datatypes.length bs1) =? n)%N); 
       simpl; intros Heq11; try (now apply C.interp_true).
 
@@ -6261,7 +6261,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0.
@@ -6591,7 +6591,7 @@ Proof.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
       intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true).
       (* BVmult *)
-      - case_eq ((a1 == a1') && (a2 == a2') (* || (a1 == a2') && (a2 == a1')*) );
+      - case_eq ((a1 =? a1') && (a2 =? a2') (* || (a1 =? a2') && (a2 =? a1')*) );
             simpl; intros Heq10; try (now apply C.interp_true).
 
         case_eq ( 
@@ -6611,7 +6611,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -6899,7 +6899,7 @@ Proof.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
       intros [ | | | | | | |[ A B | A| | | | ]|N|N|N|N|N|N|N|N| | | | ]  a1' a2' Heq9; try (intros; now apply C.interp_true).
       (* BVconcat *)
-    - case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true).
+    - case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq10; try (now apply C.interp_true).
         case_eq (
              check_concat bs1 bs2 bsres && (N.of_nat (Datatypes.length bs1) =? N)%N &&
              (N.of_nat (Datatypes.length bs2) =? n)%N
@@ -6916,7 +6916,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
@@ -7215,7 +7215,7 @@ Proof.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
       intros [ | | | | | | | | | | ]  a1'  Heq6; try (intros; now apply C.interp_true).
       (* BVextract *)
-    - case_eq ((a1 == a1')); simpl; intros Heq7; try (now apply C.interp_true).
+    - case_eq ((a1 =? a1')); simpl; intros Heq7; try (now apply C.interp_true).
         case_eq (
           check_extract bs1 bsres i (n0 + i) &&
           (N.of_nat (Datatypes.length bs1) =? n1)%N && (n0 + i <=? n1)%N
@@ -7232,7 +7232,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. easy. }
         specialize (@H0 H1). rewrite Heq6 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0.
@@ -7476,7 +7476,7 @@ Proof.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
       intros [ | | | | | | | | | | ]  a1'  Heq6; try (intros; now apply C.interp_true).
       (* BVzextend *)
-    - case_eq ((a1 == a1')); simpl; intros Heq7; try (now apply C.interp_true).
+    - case_eq ((a1 =? a1')); simpl; intros Heq7; try (now apply C.interp_true).
         case_eq (
             check_zextend bs1 bsres i && (N.of_nat (Datatypes.length bs1) =? n)%N
         ); simpl; intros Heq8; try (now apply C.interp_true).
@@ -7492,7 +7492,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. easy. }
         specialize (@H0 H1). rewrite Heq6 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0.
@@ -7722,7 +7722,7 @@ Proof.
       case_eq (t_atom .[ a]); try (intros; now apply C.interp_true).
       intros [ | | | | | | | | | | ]  a1'  Heq6; try (intros; now apply C.interp_true).
       (* BVsextend *)
-    - case_eq ((a1 == a1')); simpl; intros Heq7; try (now apply C.interp_true).
+    - case_eq ((a1 =? a1')); simpl; intros Heq7; try (now apply C.interp_true).
         case_eq (
             check_sextend bs1 bsres i && (N.of_nat (Datatypes.length bs1) =? n)%N
         ); simpl; intros Heq8; try (now apply C.interp_true).
@@ -7738,7 +7738,7 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq6. easy. }
         specialize (@H0 H1). rewrite Heq6 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0.
@@ -8045,7 +8045,7 @@ Proof.
        case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2.
        case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc.
       (* BVshl *)
-      case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true).
+      case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq10; try (now apply C.interp_true).
         case_eq (
                 check_shl bs1 bv2 bsres && (N.of_nat (Datatypes.length bs1) =? n)%N &&
                 (N.of_nat (Datatypes.length bv2) =? n)%N && (n0 =? n)%N
@@ -8062,13 +8062,13 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
 
         pose proof (H a2). 
-        assert (a2 < PArray.length t_atom).
+        assert (a2 <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heqa2, Heqc. easy. }
         specialize (@H4 H5). rewrite Heqa2 in H4. simpl in H4.
 
@@ -8375,7 +8375,7 @@ Proof.
        case_eq (t_atom .[ a2]); try (intros; now apply C.interp_true). intros c Heqa2.
        case_eq c; try (intros; now apply C.interp_true). intros bv2 n0 Heqc.
       (* BVshr *)
-      case_eq ((a1 == a1') && (a2 == a2')); simpl; intros Heq10; try (now apply C.interp_true).
+      case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq10; try (now apply C.interp_true).
         case_eq (
                 check_shr bs1 bv2 bsres && (N.of_nat (Datatypes.length bs1) =? n)%N &&
                 (N.of_nat (Datatypes.length bv2) =? n)%N && (n0 =? n)%N
@@ -8392,13 +8392,13 @@ Proof.
         rewrite aforallbi_spec;intros.
 
         pose proof (H a). 
-        assert (a < PArray.length t_atom).
+        assert (a <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. }
         specialize (@H0 H1). rewrite Heq9 in H0. simpl in H0.
         rewrite !andb_true_iff in H0. destruct H0. destruct H0.
 
         pose proof (H a2). 
-        assert (a2 < PArray.length t_atom).
+        assert (a2 <? PArray.length t_atom).
         { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heqa2, Heqc. easy. }
         specialize (@H4 H5). rewrite Heqa2 in H4. simpl in H4.
 
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index d5a9da9..d7c9731 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -474,22 +474,22 @@ Section Int63.
   Local Open Scope int63_scope.
 
   Let int_lt x y :=
-    if x < y then True else False.
+    if x <? y then True else False.
 
   Global Instance int63_ord : OrdType int.
   Proof.
     exists int_lt; unfold int_lt.
     - intros x y z.
-      case_eq (x < y); intro;
-        case_eq (y < z); intro;
-          case_eq (x < z); intro;
+      case_eq (x <? y); intro;
+        case_eq (y <? z); intro;
+          case_eq (x <? z); intro;
             simpl; try easy.
       contradict H1.
       rewrite not_false_iff_true.
       rewrite ltb_spec in *.
       exact (Z.lt_trans _ _ _ H H0).
     - intros x y.
-      case_eq (x < y); intro; simpl; try easy.
+      case_eq (x <? y); intro; simpl; try easy.
       intros.
       rewrite ltb_spec in *.
       rewrite <- Misc.to_Z_eq.
@@ -501,8 +501,8 @@ Section Int63.
   Proof.
     constructor.
     intros x y.
-    case_eq (x < y); intro;
-      case_eq (x == y); intro; unfold lt in *; simpl.
+    case_eq (x <? y); intro;
+      case_eq (x =? y); intro; unfold lt in *; simpl.
     - rewrite Int63.eqb_spec in H0.
       contradict H0.
       assert (int_lt x y). unfold int_lt.
@@ -512,7 +512,7 @@ Section Int63.
     - apply LT. unfold int_lt. rewrite H; trivial.
     - apply EQ. rewrite Int63.eqb_spec in H0; trivial.
     - apply GT. unfold int_lt.
-      case_eq (y < x); intro; simpl; try easy.
+      case_eq (y <? x); intro; simpl; try easy.
       specialize (Misc.leb_ltb_eqb x y); intro.
       contradict H2.
       rewrite Misc.leb_negb_gtb. rewrite H1. simpl.
diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v
index db6e689..bc4ab5d 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.v
@@ -23,7 +23,7 @@ Unset Strict Implicit.
 
 Definition or_of_imp args :=
   let last := PArray.length args - 1 in
-  amapi (fun i l => if i == last then l else Lit.neg l) args.
+  amapi (fun i l => if i =? last then l else Lit.neg l) args.
 (* Register or_of_imp as PrimInline. *)
 
 Lemma length_or_of_imp : forall args,
@@ -31,21 +31,21 @@ Lemma length_or_of_imp : forall args,
 Proof. intro; unfold or_of_imp; apply length_amapi. Qed.
 
 Lemma get_or_of_imp : forall args i,
-  i < (PArray.length args) - 1 -> (or_of_imp args).[i] = Lit.neg (args.[i]).
+  i <? (PArray.length args) - 1 -> (or_of_imp args).[i] = Lit.neg (args.[i]).
 Proof.
-  unfold or_of_imp; intros args i H; case_eq (0 < PArray.length args).
+  unfold or_of_imp; intros args i H; case_eq (0 <? PArray.length args).
   intro Heq; rewrite get_amapi.
-  replace (i == PArray.length args - 1) with false; auto; symmetry; rewrite eqb_false_spec; intro; subst i; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia.
+  replace (i =? PArray.length args - 1) with false; auto; symmetry; rewrite eqb_false_spec; intro; subst i; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia.
   rewrite ltb_spec; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia.
-  rewrite ltb_negb_geb; case_eq (PArray.length args <= 0); try discriminate; intros Heq _; assert (H1: PArray.length args = 0).
+  rewrite ltb_negb_geb; case_eq (PArray.length args <=? 0); try discriminate; intros Heq _; assert (H1: PArray.length args = 0).
   apply to_Z_inj; rewrite leb_spec in Heq; destruct (to_Z_bounded (PArray.length args)) as [H1 _]; change [|0|] with 0%Z in *; lia.
   rewrite !get_outofbound.
   rewrite default_amapi, H1; auto.
-  rewrite H1; case_eq (i < 0); auto; intro H2; eelim ltb_0; eassumption.
-  rewrite length_amapi, H1; case_eq (i < 0); auto; intro H2; eelim ltb_0; eassumption.
+  rewrite H1; case_eq (i <? 0); auto; intro H2; eelim ltb_0; eassumption.
+  rewrite length_amapi, H1; case_eq (i <? 0); auto; intro H2; eelim ltb_0; eassumption.
 Qed.
 
-Lemma get_or_of_imp2 : forall args i, 0 < PArray.length args ->
+Lemma get_or_of_imp2 : forall args i, 0 <? PArray.length args ->
   i = (PArray.length args) - 1 -> (or_of_imp args).[i] = args.[i].
 Proof.
   unfold or_of_imp; intros args i Heq Hi; rewrite get_amapi; subst i.
@@ -55,7 +55,7 @@ Qed.
 
 Lemma afold_right_impb p a :
   (forall x, p (Lit.neg x) = negb (p x)) ->
-  (PArray.length a == 0) = false ->
+  (PArray.length a =? 0) = false ->
   (afold_right bool true implb (amap p a)) =
   List.existsb p (to_list (or_of_imp a)).
 Proof.
@@ -97,7 +97,7 @@ Proof.
     case_eq (List.existsb p (to_list (or_of_imp a))); auto.
     rewrite existsb_exists. intros [x [H4 H5]].
     apply In_to_list in H4. destruct H4 as [i [H4 ->]].
-    case_eq (i < PArray.length a - 1); intro Heq.
+    case_eq (i <? PArray.length a - 1); intro Heq.
     + specialize (H2 i). rewrite length_amap in H2. assert (H6 := H2 Heq). rewrite get_amap in H6.
       now rewrite (get_or_of_imp Heq), Hp, H6 in H5. apply (ltb_trans _ (PArray.length a - 1)); auto.
       now apply minus_1_lt.
@@ -108,7 +108,7 @@ Proof.
         apply to_Z_inj. rewrite (to_Z_sub_1 _ 0); auto.
         rewrite ltb_spec in H4; auto.
         rewrite ltb_negb_geb in Heq.
-        case_eq (PArray.length a - 1 <= i); intro H2; rewrite H2 in Heq; try discriminate.
+        case_eq (PArray.length a - 1 <=? i); intro H2; rewrite H2 in Heq; try discriminate.
         clear Heq. rewrite leb_spec in H2. rewrite (to_Z_sub_1 _ 0) in H2; auto.
         lia.
       }
@@ -155,7 +155,7 @@ Section CHECKER.
       else l :: to_list args
     | Fimp args =>
       if Lit.is_pos l then C._true
-      else if PArray.length args == 0 then C._true
+      else if PArray.length args =? 0 then C._true
       else
         let args := or_of_imp args in
         l :: to_list args
@@ -193,7 +193,7 @@ Section CHECKER.
         if Lit.is_pos l then to_list args
         else C._true
       | Fimp args =>
-        if PArray.length args == 0 then C._true else
+        if PArray.length args =? 0 then C._true else
         if Lit.is_pos l then 
           let args := or_of_imp args in
           to_list args
@@ -271,15 +271,15 @@ Section CHECKER.
     let x := Lit.blit l in
     match get_hash x with
     | For args =>
-      if i < PArray.length args then Lit.lit x::Lit.neg (args.[i])::nil
+      if i <? PArray.length args then Lit.lit x::Lit.neg (args.[i])::nil
       else C._true
     | Fand args =>
-      if i < PArray.length args then Lit.nlit x::(args.[i])::nil
+      if i <? PArray.length args then Lit.nlit x::(args.[i])::nil
       else C._true
     | Fimp args =>
       let len := PArray.length args in
-      if i < len then
-        if i == len - 1 then Lit.lit x::Lit.neg (args.[i])::nil
+      if i <? len then
+        if i =? len - 1 then Lit.lit x::Lit.neg (args.[i])::nil
         else Lit.lit x::(args.[i])::nil
       else C._true
     | _ => C._true
@@ -297,15 +297,15 @@ Section CHECKER.
       let x := Lit.blit l in
       match get_hash x with
       | For args =>
-        if (i < PArray.length args) && negb (Lit.is_pos l) then Lit.neg (args.[i])::nil
+        if (i <? PArray.length args) && negb (Lit.is_pos l) then Lit.neg (args.[i])::nil
         else C._true
       | Fand args =>
-        if (i < PArray.length args) && (Lit.is_pos l) then (args.[i])::nil
+        if (i <? PArray.length args) && (Lit.is_pos l) then (args.[i])::nil
         else C._true
       | Fimp args =>
         let len := PArray.length args in
-        if (i < len) && negb (Lit.is_pos l) then
-          if i == len - 1 then Lit.neg (args.[i])::nil
+        if (i <? len) && negb (Lit.is_pos l) then
+          if i =? len - 1 then Lit.neg (args.[i])::nil
           else (args.[i])::nil
         else C._true
       | _ => C._true
@@ -362,7 +362,7 @@ Section CHECKER.
             tauto_check).
    - rewrite afold_left_and, C.Cinterp_neg;apply orb_negb_r.
    - rewrite afold_left_or, orb_comm;apply orb_negb_r.
-   - case_eq (PArray.length a == 0); auto using C.interp_true.
+   - case_eq (PArray.length a =? 0); auto using C.interp_true.
      intro Hl; simpl.
      unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl.
      rewrite (afold_right_impb (Lit.interp_neg _) Hl), orb_comm;try apply orb_negb_r.
@@ -381,7 +381,7 @@ Section CHECKER.
   Proof.
    unfold check_BuildProj,C.valid;intros l i.
    case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true;
-   case_eq (i < PArray.length a);intros Hlt;auto using C.interp_true;simpl.
+   case_eq (i <? PArray.length a);intros Hlt;auto using C.interp_true;simpl.
    - rewrite Lit.interp_nlit;unfold Var.interp;rewrite rho_interp, orb_false_r, H.
      simpl;rewrite afold_left_and.
      case_eq (List.forallb (Lit.interp rho) (to_list a));trivial.
@@ -394,9 +394,9 @@ Section CHECKER.
      case_eq (Lit.interp rho (a .[ i]));trivial.
      intros Heq Hex;elim Hex;exists (a.[i]);split;trivial.
      apply to_list_In; auto.
-   - assert (Hl : (PArray.length a == 0) = false)
+   - assert (Hl : (PArray.length a =? 0) = false)
        by (rewrite eqb_false_spec; intro H1; rewrite H1 in Hlt; now elim (ltb_0 i)).
-     case_eq (i == PArray.length a - 1);intros Heq;simpl;
+     case_eq (i =? PArray.length a - 1);intros Heq;simpl;
        rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, H;simpl.
      + rewrite Lit.interp_neg, orb_false_r.
        rewrite (afold_right_impb (Lit.interp_neg _) Hl).
@@ -452,9 +452,9 @@ Section CHECKER.
    tauto_check.
    - rewrite afold_left_and, C.Cinterp_neg, orb_false_r;trivial.
    - rewrite afold_left_or, orb_false_r;trivial.
-   - case_eq (PArray.length a == 0); auto using C.interp_true.
+   - case_eq (PArray.length a =? 0); auto using C.interp_true.
      intro Hl. now rewrite orb_false_r, (afold_right_impb (Lit.interp_neg _) Hl).
-   - case_eq (PArray.length a == 0); auto using C.interp_true.
+   - case_eq (PArray.length a =? 0); auto using C.interp_true.
   Qed.
 
   Lemma valid_check_ImmBuildDef2 : forall cid, C.valid rho (check_ImmBuildDef2 cid).
@@ -475,7 +475,7 @@ Section CHECKER.
    destruct (S.get s cid) as [ | l [ | _l _c]];auto using C.interp_true.
    simpl;unfold Lit.interp, Var.interp; rewrite !rho_interp;
      destruct (t_form.[Lit.blit l]);auto using C.interp_true;
-       case_eq (i < PArray.length a); intros Hlt;auto using C.interp_true;
+       case_eq (i <? PArray.length a); intros Hlt;auto using C.interp_true;
        case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl;
        rewrite !orb_false_r.  
    - rewrite afold_left_and.
@@ -487,17 +487,17 @@ Section CHECKER.
      intros Heq' Hex;elim Hex;exists (a.[i]);split;trivial.
      apply to_list_In; auto.
    - rewrite negb_true_iff, <-not_true_iff_false.
-     assert (Hl:(PArray.length a == 0) = false)
+     assert (Hl:(PArray.length a =? 0) = false)
        by (rewrite eqb_false_spec; intro H; rewrite H in Hlt; now apply (ltb_0 i)).
      rewrite (afold_right_impb (Lit.interp_neg _) Hl).
-     case_eq (i == PArray.length a - 1);intros Heq';simpl;
+     case_eq (i =? PArray.length a - 1);intros Heq';simpl;
        unfold C.interp;simpl;try rewrite Lit.interp_neg;rewrite orb_false_r,
                                                         existsb_exists;case_eq (Lit.interp rho (a .[ i]));trivial;
          intros Heq2 Hex;elim Hex.
      exists (a.[i]);split;trivial.
-     assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto.
+     assert (H1: 0 <? PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto.
      exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial.
-     assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; lia); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto.
+     assert (H1: i <? PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; lia); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto.
   Qed.
 
 End CHECKER.
diff --git a/src/euf/Euf.v b/src/euf/Euf.v
index 6b97f94..fae0cfd 100644
--- a/src/euf/Euf.v
+++ b/src/euf/Euf.v
@@ -40,23 +40,23 @@ Section certif.
     | nil =>
       let xres := Lit.blit res in
       get_eq xres (fun t1' t2' =>
-         if ((t1 == t1') && (t2 == t2')) ||
-            ((t1 == t2') && (t2 == t1')) then
+         if ((t1 =? t1') && (t2 =? t2')) ||
+            ((t1 =? t2') && (t2 =? t1')) then
             Lit.lit xres :: clause
          else C._true)
     | leq::eqs =>
       let xeq := Lit.blit leq in
       get_eq xeq (fun t t' =>
-          if t2 == t' then
+          if t2 =? t' then
             check_trans_aux t1 t eqs res (Lit.nlit xeq :: clause)
           else
-            if t2 == t then
+            if t2 =? t then
               check_trans_aux t1 t' eqs res (Lit.nlit xeq :: clause)
             else
-              if t1 == t' then
+              if t1 =? t' then
                 check_trans_aux t t2 eqs res (Lit.nlit xeq :: clause)
               else
-                if t1 == t then
+                if t1 =? t then
                   check_trans_aux t' t2 eqs res (Lit.nlit xeq :: clause)
                 else C._true)
     end.
@@ -66,7 +66,7 @@ Section certif.
     | nil =>
       let xres := Lit.blit res in
         get_eq xres (fun t1 t2 =>
-         if t1 == t2 then Lit.lit xres :: nil else C._true)
+         if t1 =? t2 then Lit.lit xres :: nil else C._true)
     | leq :: eqs =>
       let xeq := Lit.blit leq in
       get_eq xeq
@@ -79,12 +79,12 @@ Section certif.
     | nil, nil, nil => c
     | eq::eqs, t1::l, t2::r =>
       match eq with
-      | None => if t1 == t2 then build_congr eqs l r c else C._true
+      | None => if t1 =? t2 then build_congr eqs l r c else C._true
       | Some leq =>
         let xeq := Lit.blit leq in
         get_eq xeq (fun t1' t2' =>
-          if ((t1 == t1') && (t2 == t2')) ||
-             ((t1 == t2') && (t2 == t1')) then
+          if ((t1 =? t1') && (t2 =? t2')) ||
+             ((t1 =? t2') && (t2 =? t1')) then
             build_congr eqs l r (Lit.nlit xeq :: c)
           else C._true)
       end
@@ -104,7 +104,7 @@ Section certif.
            build_congr eqs (a::nil) (b::nil) (Lit.lit xeq :: nil)
         else C._true
       | Atom.Aapp f1 args1, Atom.Aapp f2 args2 =>
-        if f1 == f2 then build_congr eqs args1 args2 (Lit.lit xeq :: nil)
+        if f1 =? f2 then build_congr eqs args1 args2 (Lit.lit xeq :: nil)
         else C._true
       | _, _ => C._true
       end).
@@ -126,7 +126,7 @@ Section certif.
           (a::nil) (b::nil) (Lit.nlit xPA :: Lit.lit xPB :: nil)
         else C._true
       | Atom.Aapp p a, Atom.Aapp p' b =>
-        if p == p' then
+        if p =? p' then
           build_congr eqs a b (Lit.nlit xPA :: Lit.lit xPB :: nil)
         else C._true
       | _, _ => C._true
@@ -215,7 +215,7 @@ Section certif.
       destruct b;trivial with smtcoq_euf.
       generalize wt_t_atom;unfold Atom.wt;unfold is_true;
        rewrite Misc.aforallbi_spec;intros.
-      assert (i < length t_atom).
+      assert (i <? length t_atom).
         apply PArray.get_not_default_lt.
         rewrite H0, def_t_atom;discriminate.
       apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2.
@@ -477,10 +477,10 @@ Section certif.
       rewrite !wf_interp_form, H, H0;simpl.
       generalize wt_t_atom;unfold Atom.wt;unfold is_true;
        rewrite Misc.aforallbi_spec;intros.
-      assert (i < length t_atom).
+      assert (i <? length t_atom).
         apply PArray.get_not_default_lt.
         rewrite H1, def_t_atom;discriminate.
-      assert (i0 < length t_atom).
+      assert (i0 <? length t_atom).
         apply PArray.get_not_default_lt.
         rewrite H2, def_t_atom;discriminate.
       apply H4 in H5;apply H4 in H6;clear H4.
@@ -498,10 +498,10 @@ Section certif.
       rewrite !wf_interp_form, H, H0;simpl.
       generalize wt_t_atom;unfold Atom.wt;unfold is_true;
        rewrite Misc.aforallbi_spec;intros.
-      assert (i < length t_atom).
+      assert (i <? length t_atom).
         apply PArray.get_not_default_lt.
         rewrite H1, def_t_atom. discriminate.
-      assert (i0 < length t_atom).
+      assert (i0 <? length t_atom).
         apply PArray.get_not_default_lt.
         rewrite H2, def_t_atom;discriminate.
       apply H4 in H5;apply H4 in H6;clear H4.
@@ -520,10 +520,10 @@ Section certif.
       rewrite !wf_interp_form, H, H0;simpl.
       generalize wt_t_atom;unfold Atom.wt;unfold is_true;
        rewrite Misc.aforallbi_spec;intros.
-      assert (i < length t_atom).
+      assert (i <? length t_atom).
         apply PArray.get_not_default_lt.
         rewrite H1, def_t_atom;discriminate.
-      assert (i0 < length t_atom).
+      assert (i0 <? length t_atom).
         apply PArray.get_not_default_lt.
         rewrite H2, def_t_atom;discriminate.
       apply H4 in H5;apply H4 in H6;clear H4.
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index 19c12d8..182a4fc 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -360,15 +360,15 @@ Section certif.
   Definition check_diseq l : C.t :=
     match get_form (Lit.blit l) with
       |Form.For a =>
-        if PArray.length a == 3 then
+        if PArray.length a =? 3 then
           let a_eq_b := a.[0] in
           let not_a_le_b := a.[1] in
           let not_b_le_a := a.[2] in
           get_eq a_eq_b (fun a b => get_not_le not_a_le_b (fun a' b' => get_not_le not_b_le_a (fun b'' a'' =>
-            if (a == a') && (a == a'') && (b == b') && (b == b'')
+            if (a =? a') && (a =? a'') && (b =? b') && (b =? b'')
               then (Lit.lit (Lit.blit l))::nil
               else
-                if (a == b') && (a == b'') && (b == a') && (b == a'')
+                if (a =? b') && (a =? b'') && (b =? a') && (b =? a'')
                   then (Lit.lit (Lit.blit l))::nil
                   else C._true)))
           else C._true
@@ -668,7 +668,7 @@ Section certif.
    Lemma build_pexpr_atom_aux_correct :
       forall (build_pexpr : vmap -> hatom -> vmap * PExpr Z) h i,
         (forall h' vm vm' pe,
-          h' < h ->
+          h' <? h ->
           Typ.eqb (get_type t_i t_func t_atom h') Typ.TZ ->
           build_pexpr vm h' = (vm',pe) ->
           wf_vmap vm ->
@@ -681,7 +681,7 @@ Section certif.
           bounded_pexpr (fst vm') pe /\
           t_interp.[h'] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe))->
         forall a vm vm' pe,
-          h < i ->
+          h <? i ->
           lt_atom h a ->
           check_atom a Typ.TZ ->
           build_pexpr_atom_aux build_pexpr vm a = (vm',pe) ->
@@ -933,7 +933,7 @@ Transparent build_z_atom.
           t_interp.[h] = Bval t_i Typ.TZ (Zeval_expr (interp_vmap vm') pe).
    Proof.
      intros.
-     case_eq (h < length t_atom);intros.
+     case_eq (h <? length t_atom);intros.
      apply build_pexpr_correct_aux;trivial.
      rewrite <- ltb_spec;trivial.
      revert H;unfold get_type,get_type'.
@@ -1044,7 +1044,7 @@ Transparent build_z_atom.
       intros;apply build_formula_atom_correct with
         (get_type t_i t_func t_atom h);trivial.
       unfold wt, is_true in wt_t_atom;rewrite aforallbi_spec in wt_t_atom.
-      case_eq (h < length t_atom);intros Heq;unfold get_type;auto with smtcoq_core.
+      case_eq (h <? length t_atom);intros Heq;unfold get_type;auto with smtcoq_core.
       unfold get_type'.
       rewrite !PArray.get_outofbound, default_t_interp, def_t_atom;trivial; try reflexivity.
       rewrite length_t_interp;trivial.
@@ -1188,7 +1188,7 @@ Transparent build_z_atom.
       (* Fnot2 *)
       case_eq (build_var vm (Lit.blit l)); try discriminate; intros [vm0 f] Heq H H1; inversion H; subst vm0; subst bf; destruct (Hbv _ _ _ _ Heq H1) as [H2 [H3 [H4 [H5 H6]]]]; do 3 (split; auto); case_eq (Lit.is_pos l); [apply build_not2_pos_correct|apply build_not2_neg_correct]; auto.
       (* Fand *)
-      simpl; unfold afold_left; rewrite !length_amap; case_eq (length l == 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl.
+      simpl; unfold afold_left; rewrite !length_amap; case_eq (length l =? 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl.
       intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core).
       revert vm' bf; rewrite !get_amap by exact Hl; set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern (length l), a, b; subst a b; apply foldi_ind2.
       rewrite ltb_spec, to_Z_0 in Hl; rewrite leb_spec, to_Z_1; lia.
@@ -1201,7 +1201,7 @@ Transparent build_z_atom.
       simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto with smtcoq_core.
       simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; rewrite get_amap by exact H1; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite andb_true_r; try rewrite andb_false_r; try (intros; split; auto with smtcoq_core); try discriminate; intros [H20 H21]; auto with smtcoq_core.
       (* For *)
-      simpl; unfold afold_left; rewrite !length_amap; case_eq (length l == 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl.
+      simpl; unfold afold_left; rewrite !length_amap; case_eq (length l =? 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl.
       intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core); discriminate.
       revert vm' bf; rewrite !get_amap by exact Hl; set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern (length l), a, b; subst a b; apply foldi_ind2.
       rewrite ltb_spec, to_Z_0 in Hl; rewrite leb_spec, to_Z_1; lia.
@@ -1215,7 +1215,7 @@ Transparent build_z_atom.
       simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; rewrite get_amap by exact H1; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite orb_false_r; try rewrite orb_true_r; auto with smtcoq_core; try (intros [H20|H20]; auto with smtcoq_core; discriminate); right; intro H20; discriminate.
       (* Fimp *)
       {
-      simpl; unfold afold_right; rewrite !length_amap; case_eq (length l == 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl.
+      simpl; unfold afold_right; rewrite !length_amap; case_eq (length l =? 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl.
       intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core).
       revert vm' bf; rewrite !get_amap by (apply minus_1_lt; rewrite eqb_false_spec, not_0_ltb; exact Hl); set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern (length l), a, b; subst a b; apply foldi_ind2.
       rewrite ltb_spec, to_Z_0 in Hl; rewrite leb_spec, to_Z_1; lia.
@@ -1449,7 +1449,7 @@ Transparent build_z_atom.
      destruct b; try (apply valid_C_true; trivial).
      generalize wt_t_atom;unfold Atom.wt;unfold is_true;
        rewrite aforallbi_spec;intros.
-     assert (i < length t_atom).
+     assert (i <? length t_atom).
      apply PArray.get_not_default_lt.
      rewrite H0, def_t_atom;discriminate.
      apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2.
@@ -1480,7 +1480,7 @@ Transparent build_z_atom.
      destruct b; try (apply valid_C_true; trivial).
      generalize wt_t_atom;unfold Atom.wt;unfold is_true;
        rewrite aforallbi_spec;intros.
-     assert (i < length t_atom).
+     assert (i <? length t_atom).
      apply PArray.get_not_default_lt.
      rewrite H0, def_t_atom;discriminate.
      apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2.
@@ -1548,12 +1548,12 @@ Transparent build_z_atom.
    Proof.
      unfold check_diseq; intro c.
      case_eq (t_form.[Lit.blit c]);intros;subst; try (unfold C.valid; apply valid_C_true; trivial).
-     case_eq ((length a) == 3); intros; try (unfold C.valid; apply valid_C_true; trivial).
+     case_eq ((length a) =? 3); intros; try (unfold C.valid; apply valid_C_true; trivial).
      apply eqb_correct in H0.
      apply get_eq_interp; intros.
      apply get_not_le_interp; intros.
      apply get_not_le_interp; intros.
-     case_eq ((a0 == a1) && (a0 == b1) && (b == b0) && (b == a2)); intros; subst;
+     case_eq ((a0 =? a1) && (a0 =? b1) && (b =? b0) && (b =? a2)); intros; subst;
        try (unfold C.valid; apply valid_C_true; trivial).
      repeat(apply andb_prop in H19; destruct H19).
      apply Int63.eqb_spec in H19;apply Int63.eqb_spec in H20;apply Int63.eqb_spec in H21;apply Int63.eqb_spec in H22; subst a0 b.
@@ -1598,7 +1598,7 @@ Transparent build_z_atom.
        unfold interp_hatom in H21; do 2 rewrite t_interp_wf in H21; trivial.
      trivial.
      destruct H19.
-     case_eq ((a0 == b0) && (a0 == a2) && (b == a1) && (b == b1)); intros; subst;
+     case_eq ((a0 =? b0) && (a0 =? a2) && (b =? a1) && (b =? b1)); intros; subst;
        try (unfold C.valid; apply valid_C_true; trivial).
      repeat(apply andb_prop in H19; destruct H19).
      apply Int63.eqb_spec in H19;apply Int63.eqb_spec in H20;apply Int63.eqb_spec in H21;apply Int63.eqb_spec in H22;subst a0 b.
diff --git a/src/spl/Assumptions.v b/src/spl/Assumptions.v
index 0a8d79e..102148d 100644
--- a/src/spl/Assumptions.v
+++ b/src/spl/Assumptions.v
@@ -65,7 +65,7 @@ Section Checker.
   End Forallb2.
 
   Definition check_hole (s:S.t) (prem_id:list clause_id) (prem:list C.t) (concl:C.t) : C.t :=
-    if forallb2 (fun id c => forallb2 (fun i j => i == j) (S.get s id) (S.sort_uniq c)) prem_id prem
+    if forallb2 (fun id c => forallb2 (fun i j => i =? j) (S.get s id) (S.sort_uniq c)) prem_id prem
     then concl
     else C._true.
 
@@ -89,7 +89,7 @@ Section Checker_correct.
              t_form).
 
   Lemma interp_check_clause c1 : forall c2,
-    forallb2 (fun i j => i == j) c1 c2 -> C.interp rho c1 = C.interp rho c2.
+    forallb2 (fun i j => i =? j) c1 c2 -> C.interp rho c1 = C.interp rho c2.
   Proof.
     induction c1 as [ |l1 c1 IHc1]; simpl; intros [ |l2 c2]; simpl; auto; try discriminate.
     unfold is_true. rewrite andb_true_iff. intros [H1 H2].
@@ -97,7 +97,7 @@ Section Checker_correct.
   Qed.
 
   Lemma valid_check_clause cid c :
-    forallb2 (fun i j => i == j) (S.get s cid) (S.sort_uniq c) ->
+    forallb2 (fun i j => i =? j) (S.get s cid) (S.sort_uniq c) ->
     interp_uf rho c.
   Proof.
     intro H. rewrite <- interp_equiv, <- S.sort_uniq_correct; auto.
@@ -131,7 +131,7 @@ Section Checker_correct.
     - unfold C.valid. now rewrite interp_equiv.
     - now apply C.interp_true.
     - now apply C.interp_true.
-    - case_eq (forallb2 (fun i j => i == j) (S.get s pid) (S.sort_uniq p));
+    - case_eq (forallb2 (fun i j => i =? j) (S.get s pid) (S.sort_uniq p));
       simpl; intro Heq; [ |now apply C.interp_true].
       apply IHpids. apply H. apply (valid_check_clause _ _ Heq).
   Qed.
diff --git a/src/spl/Operators.v b/src/spl/Operators.v
index 540de3f..95bbe8e 100644
--- a/src/spl/Operators.v
+++ b/src/spl/Operators.v
@@ -35,7 +35,7 @@ Section Operators.
   Fixpoint check_in x l :=
     match l with
       | nil => false
-      | t::q => if x == t then true else check_in x q
+      | t::q => if x =? t then true else check_in x q
     end.
 
 
@@ -43,7 +43,7 @@ Section Operators.
   Proof.
     intro x; induction l as [ |t q IHq]; simpl.
     split; intro H; try discriminate; elim H.
-    case_eq (x == t).
+    case_eq (x =? t).
     rewrite eqb_spec; intro; subst t; split; auto.
     intro H; rewrite IHq; split; auto; intros [H1|H1]; auto; rewrite H1, eqb_refl in H; discriminate.
   Qed.
@@ -54,7 +54,7 @@ Section Operators.
       | nil => true
       | b::q => if aexistsbi (fun _ (x:option (int*int)) =>
         match x with
-          | Some (a',b') => ((a == a') && (b == b')) || ((a == b') && (b == a'))
+          | Some (a',b') => ((a =? a') && (b =? b')) || ((a =? b') && (b =? a'))
           | None => false
         end
       ) t then check_diseqs_complete_aux a q t else false
@@ -63,13 +63,13 @@ Section Operators.
 
   Lemma check_diseqs_complete_aux_spec : forall a dist t,
     check_diseqs_complete_aux a dist t = true <->
-    forall y, In y dist -> exists i, i < length t /\
+    forall y, In y dist -> exists i, i <? length t /\
       (t.[i] = Some (a,y) \/ t.[i] = Some (y,a)).
   Proof.
     intros a dist t; induction dist as [ |b q IHq]; simpl; split; auto.
     intros _ y H; inversion H.
-    case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t); try discriminate; rewrite aexistsbi_spec; intros [i [H1 H2]]; rewrite IHq; clear IHq; intros H3 y [H4|H4]; auto; subst y; exists i; split; auto; generalize H2; case (t .[ i]); try discriminate; intros [a' b']; rewrite orb_true_iff, !andb_true_iff, !Int63.eqb_spec; intros [[H4 H5]|[H4 H5]]; subst a' b'; auto.
-    intro H1; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t).
+    case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t); try discriminate; rewrite aexistsbi_spec; intros [i [H1 H2]]; rewrite IHq; clear IHq; intros H3 y [H4|H4]; auto; subst y; exists i; split; auto; generalize H2; case (t .[ i]); try discriminate; intros [a' b']; rewrite orb_true_iff, !andb_true_iff, !Int63.eqb_spec; intros [[H4 H5]|[H4 H5]]; subst a' b'; auto.
+    intro H1; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t).
     intros _; rewrite IHq; clear IHq; intros y Hy; apply H1; auto.
     rewrite aexistsbi_false_spec; destruct (H1 b (or_introl (refl_equal b))) as [i [H2 H3]]; intro H; rewrite <- (H _ H2); destruct H3 as [H3|H3]; rewrite H3; rewrite !eqb_refl; auto; rewrite orb_true_r; auto.
   Qed.
@@ -77,15 +77,15 @@ Section Operators.
 
   Lemma check_diseqs_complete_aux_false_spec : forall a dist t,
     check_diseqs_complete_aux a dist t = false <->
-    exists y, In y dist /\ forall i, i < length t ->
+    exists y, In y dist /\ forall i, i <? length t ->
       (t.[i] <> Some (a,y) /\ t.[i] <> Some (y,a)).
   Proof.
     intros a dist t; induction dist as [ |b q IHq]; simpl; split; try discriminate.
     intros [y [H _]]; elim H.
-    case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t).
+    case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t).
     intros _; rewrite IHq; clear IHq; intros [y [H3 H4]]; exists y; auto.
     rewrite aexistsbi_false_spec; intros H _; exists b; split; auto; intros i Hi; split; intro H1; generalize (H _ Hi); rewrite H1, !eqb_refl; try discriminate; rewrite orb_true_r; discriminate.
-    intros [y [H1 H2]]; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a == a') && (b == b') || (a == b') && (b == a') | None => false end) t); auto; rewrite aexistsbi_spec; intros [i [H3 H4]]; rewrite IHq; clear IHq; exists y; destruct H1 as [H1|H1]; auto; subst y; case_eq (t.[i]); [intros [a' b'] Heq|intro Heq]; rewrite Heq in H4; try discriminate; rewrite orb_true_iff, !andb_true_iff, !eqb_spec in H4; destruct H4 as [[H4 H5]|[H4 H5]]; subst a' b'; generalize (H2 _ H3); rewrite Heq; intros [H4 H5]; [elim H4|elim H5]; auto.
+    intros [y [H1 H2]]; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t); auto; rewrite aexistsbi_spec; intros [i [H3 H4]]; rewrite IHq; clear IHq; exists y; destruct H1 as [H1|H1]; auto; subst y; case_eq (t.[i]); [intros [a' b'] Heq|intro Heq]; rewrite Heq in H4; try discriminate; rewrite orb_true_iff, !andb_true_iff, !eqb_spec in H4; destruct H4 as [[H4 H5]|[H4 H5]]; subst a' b'; generalize (H2 _ H3); rewrite Heq; intros [H4 H5]; [elim H4|elim H5]; auto.
   Qed.
 
 
@@ -98,7 +98,7 @@ Section Operators.
 
   Lemma check_diseqs_complete_spec : forall dist t,
     check_diseqs_complete dist t = true <->
-    forall x y, In2 x y dist -> exists i, i < length t /\
+    forall x y, In2 x y dist -> exists i, i <? length t /\
       (t.[i] = Some (x,y) \/ t.[i] = Some (y,x)).
   Proof.
     intros dist t; induction dist as [ |a q IHq]; simpl; split; auto.
@@ -112,7 +112,7 @@ Section Operators.
 
   Lemma check_diseqs_complete_false_spec : forall dist t,
     check_diseqs_complete dist t = false <->
-    exists x y, In2 x y dist /\ forall i, i < length t ->
+    exists x y, In2 x y dist /\ forall i, i <? length t ->
       (t.[i] <> Some (x,y) /\ t.[i] <> Some (y,x)).
   Proof.
     intros dist t; induction dist as [ |a q IHq]; simpl; split; try discriminate.
@@ -135,7 +135,7 @@ Section Operators.
           | Fatom a =>
             match get_atom a with
               | Atom.Abop (Atom.BO_eq A) h1 h2 =>
-                if (Typ.eqb ty A) && (negb (h1 == h2)) && (check_in h1 dist) && (check_in h2 dist) then
+                if (Typ.eqb ty A) && (negb (h1 =? h2)) && (check_in h1 dist) && (check_in h2 dist) then
                   Some (h1,h2)
                 else
                   None
@@ -150,14 +150,14 @@ Section Operators.
 
   Lemma check_diseqs_spec : forall A dist diseq,
     check_diseqs A dist diseq = true <->
-    ((forall i, i < length diseq ->
+    ((forall i, i <? length diseq ->
       let t := diseq.[i] in
         ~ Lit.is_pos t /\
         exists a, get_form (Lit.blit t) = Fatom a /\
           exists h1 h2, get_atom a = Atom.Abop (Atom.BO_eq A) h1 h2 /\
             h1 <> h2 /\ (In2 h1 h2 dist \/ In2 h2 h1 dist))
     /\
-    (forall x y, In2 x y dist -> exists i, i < length diseq /\
+    (forall x y, In2 x y dist -> exists i, i <? length diseq /\
       let t := diseq.[i] in
         ~ Lit.is_pos t /\
         exists a, get_form (Lit.blit t) = Fatom a /\
@@ -169,14 +169,14 @@ Section Operators.
      aforallbi_spec, check_diseqs_complete_spec, length_amap; split; intros [H1 H2]; split.
     clear H2; intros i Hi; generalize (H1 _ Hi); rewrite get_amap; 
     auto; case_eq (Lit.is_pos (diseq .[ i])); try discriminate; intro Heq1; case_eq (get_form (Lit.blit (diseq .[ i]))); 
-    try discriminate; intros a Heq2; case_eq (get_atom a); try discriminate; intros [ | | | | | | | B | | | | | | | | | | | | ]; try discriminate; intros h1 h2 Heq3; case_eq (Typ.eqb A B); try discriminate; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try discriminate; rewrite eqb_false_spec; intro H2; case_eq (check_in h1 dist); try discriminate; case_eq (check_in h2 dist); try discriminate; rewrite !check_in_spec; intros H3 H4 _; split; try discriminate; exists a; split; auto; exists h1, h2; repeat split; auto; rewrite <- In2_In; auto.
+    try discriminate; intros a Heq2; case_eq (get_atom a); try discriminate; intros [ | | | | | | | B | | | | | | | | | | | | ]; try discriminate; intros h1 h2 Heq3; case_eq (Typ.eqb A B); try discriminate; change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 =? h2); try discriminate; rewrite eqb_false_spec; intro H2; case_eq (check_in h1 dist); try discriminate; case_eq (check_in h2 dist); try discriminate; rewrite !check_in_spec; intros H3 H4 _; split; try discriminate; exists a; split; auto; exists h1, h2; repeat split; auto; rewrite <- In2_In; auto.
     clear H1; intros x y Hxy; destruct (H2 _ _ Hxy) as [i [H1 H4]]; clear H2; rewrite get_amap in H4; auto; exists i; split; auto; generalize H4; 
     
-    case_eq (Lit.is_pos (diseq .[ i])); intro Heq; try (intros [H|H]; discriminate); case_eq (get_form (Lit.blit (diseq .[ i]))); [intros a| | |intros a1 a2|intros a1|intros a1|intros a1|intros a1 a2|intros a1 a2| intros a1 a2 a3|intros a ls]; intro Heq2; try (intros [H|H]; discriminate); case_eq (get_atom a); [intros a1|intros a1 a2|intros [ | | | | | | | B | | | | | | | | | | | | ] h1 h2|intros a1 a2|intros a1 a2 | intros a1 a2]; intro Heq3; try (intros [H|H]; discriminate); try (case_eq (Typ.eqb A B); try (intros _ [H|H]; discriminate); change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 == h2); try (intros _ [H|H]; discriminate); rewrite eqb_false_spec; intro H10; case (check_in h1 dist); try (intros [H|H]; discriminate); case (check_in h2 dist); try (intros [H|H]; discriminate); simpl; intro H3; split; try discriminate; exists a; split; auto; destruct H3 as [H3|H3]; inversion H3; subst; auto).
+    case_eq (Lit.is_pos (diseq .[ i])); intro Heq; try (intros [H|H]; discriminate); case_eq (get_form (Lit.blit (diseq .[ i]))); [intros a| | |intros a1 a2|intros a1|intros a1|intros a1|intros a1 a2|intros a1 a2| intros a1 a2 a3|intros a ls]; intro Heq2; try (intros [H|H]; discriminate); case_eq (get_atom a); [intros a1|intros a1 a2|intros [ | | | | | | | B | | | | | | | | | | | | ] h1 h2|intros a1 a2|intros a1 a2 | intros a1 a2]; intro Heq3; try (intros [H|H]; discriminate); try (case_eq (Typ.eqb A B); try (intros _ [H|H]; discriminate); change (Typ.eqb A B = true) with (is_true (Typ.eqb A B)); rewrite Typ.eqb_spec; intro; subst B; case_eq (h1 =? h2); try (intros _ [H|H]; discriminate); rewrite eqb_false_spec; intro H10; case (check_in h1 dist); try (intros [H|H]; discriminate); case (check_in h2 dist); try (intros [H|H]; discriminate); simpl; intro H3; split; try discriminate; exists a; split; auto; destruct H3 as [H3|H3]; inversion H3; subst; auto).
 intros. destruct H0; now contradict H0.
     
-    clear H2; intros i Hi; rewrite get_amap; auto; destruct (H1 _ Hi) as [H2 [a [H3 [h1 [h2 [H4 [H5 H6]]]]]]]; clear H1; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); rewrite H3, H4, Typ.eqb_refl; simpl; replace (h1 == h2) with false by (case_eq (h1 == h2); auto; rewrite eqb_spec; intro H; elim H5; auto); simpl; rewrite <- In2_In, <- !check_in_spec in H6; auto; destruct H6 as [H6 H7]; rewrite H6, H7; auto.
-    clear H1; intros x y Hxy; destruct (H2 _ _ Hxy) as [i [H1 [H3 [a [H4 [H6 H5]]]]]]; clear H2; exists i; split; auto; rewrite get_amap; auto; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); rewrite H4; assert (H7 := or_introl (In2 y x dist) Hxy); rewrite <- In2_In, <- !check_in_spec in H7; auto; destruct H7 as [H7 H8]; destruct H5 as [H5|H5]; rewrite H5, Typ.eqb_refl; [replace (x == y) with false by (case_eq (x == y); auto; rewrite eqb_spec; auto)|replace (y == x) with false by (case_eq (y == x); auto; rewrite eqb_spec; auto)]; simpl; rewrite H7, H8; auto.
+    clear H2; intros i Hi; rewrite get_amap; auto; destruct (H1 _ Hi) as [H2 [a [H3 [h1 [h2 [H4 [H5 H6]]]]]]]; clear H1; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); rewrite H3, H4, Typ.eqb_refl; simpl; replace (h1 =? h2) with false by (case_eq (h1 =? h2); auto; rewrite eqb_spec; intro H; elim H5; auto); simpl; rewrite <- In2_In, <- !check_in_spec in H6; auto; destruct H6 as [H6 H7]; rewrite H6, H7; auto.
+    clear H1; intros x y Hxy; destruct (H2 _ _ Hxy) as [i [H1 [H3 [a [H4 [H6 H5]]]]]]; clear H2; exists i; split; auto; rewrite get_amap; auto; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); rewrite H4; assert (H7 := or_introl (In2 y x dist) Hxy); rewrite <- In2_In, <- !check_in_spec in H7; auto; destruct H7 as [H7 H8]; destruct H5 as [H5|H5]; rewrite H5, Typ.eqb_refl; [replace (x =? y) with false by (case_eq (x =? y); auto; rewrite eqb_spec; auto)|replace (y =? x) with false by (case_eq (y =? x); auto; rewrite eqb_spec; auto)]; simpl; rewrite H7, H8; auto.
   Qed.
 
 
@@ -187,7 +187,7 @@ intros. destruct H0; now contradict H0.
   (*         | Fatom a => *)
   (*           match get_atom a with *)
   (*             | Atom.Abop (Atom.BO_eq A) h1 h2 => *)
-  (*               (Typ.eqb ty A) && (negb (h1 == h2)) && (check_in h1 dist) && (check_in h2 dist) *)
+  (*               (Typ.eqb ty A) && (negb (h1 =? h2)) && (check_in h1 dist) && (check_in h2 dist) *)
   (*             | _ => false *)
   (*           end *)
   (*         | _ => false *)
@@ -195,7 +195,7 @@ intros. destruct H0; now contradict H0.
 
 
   (* Lemma check_diseqs_spec : forall A dist diseq, *)
-  (*   check_diseqs A dist diseq <-> forall i, i < length diseq -> *)
+  (*   check_diseqs A dist diseq <-> forall i, i <? length diseq -> *)
   (*     let t := diseq.[i] in *)
   (*     ~ Lit.is_pos t /\ *)
   (*     exists a, get_form (Lit.blit t) = Fatom a /\ *)
@@ -204,7 +204,7 @@ intros. destruct H0; now contradict H0.
   (* Proof. *)
   (*   intros A dist diseq; unfold check_diseqs; unfold is_true at 1; rewrite PArray.forallb_spec; split. *)
   (*   intros H i Hi; generalize (H _ Hi); clear H; case (Lit.is_pos (diseq .[ i])); try discriminate; case (get_form (Lit.blit (diseq .[ i]))); try discriminate; intros a H1; split; try discriminate; exists a; split; auto; generalize H1; clear H1; case (get_atom a); try discriminate; intros [ | | | | | | |B] h1 h2; try discriminate; rewrite !andb_true_iff; change (check_in h1 dist = true) with (is_true (check_in h1 dist)); change (check_in h2 dist = true) with (is_true (check_in h2 dist)); rewrite !check_in_spec; intros [[[H1 H4] H2] H3]; change (is_true (Typ.eqb A B)) in H1; rewrite Typ.eqb_spec in H1; subst B; exists h1; exists h2; split; auto; assert (H5: h1 <> h2) by (intro H; rewrite H, eqb_refl in H4; discriminate); split; auto; rewrite <- In2_In; auto. *)
-  (*   intros H i Hi; generalize (H _ Hi); clear H; case (Lit.is_pos (diseq .[ i])); try (intros [H _]; elim H; reflexivity); intros [_ [a [H1 [h1 [h2 [H2 [H3 H4]]]]]]]; rewrite H1, H2; rewrite !andb_true_iff; rewrite <- (In2_In H3) in H4; destruct H4 as [H4 H5]; change (check_in h1 dist = true) with (is_true (check_in h1 dist)); change (check_in h2 dist = true) with (is_true (check_in h2 dist)); rewrite !check_in_spec; repeat split; auto; case_eq (h1 == h2); auto; try (rewrite Typ.eqb_refl; auto); rewrite eqb_spec; intro; subst h1; elim H3; auto. *)
+  (*   intros H i Hi; generalize (H _ Hi); clear H; case (Lit.is_pos (diseq .[ i])); try (intros [H _]; elim H; reflexivity); intros [_ [a [H1 [h1 [h2 [H2 [H3 H4]]]]]]]; rewrite H1, H2; rewrite !andb_true_iff; rewrite <- (In2_In H3) in H4; destruct H4 as [H4 H5]; change (check_in h1 dist = true) with (is_true (check_in h1 dist)); change (check_in h2 dist = true) with (is_true (check_in h2 dist)); rewrite !check_in_spec; repeat split; auto; case_eq (h1 =? h2); auto; try (rewrite Typ.eqb_refl; auto); rewrite eqb_spec; intro; subst h1; elim H3; auto. *)
   (* Qed. *)
 
 
@@ -231,7 +231,7 @@ intros. destruct H0; now contradict H0.
     match get_form f1, get_form f2 with
       | Fatom ha, Fatom hb =>
         match get_atom ha, get_atom hb with
-          | Atom.Anop (Atom.NO_distinct ty) (x::y::nil), Atom.Abop (Atom.BO_eq ty') x' y' => (Typ.eqb ty ty') && (((x == x') && (y == y')) || ((x == y') && (y == x')))
+          | Atom.Anop (Atom.NO_distinct ty) (x::y::nil), Atom.Abop (Atom.BO_eq ty') x' y' => (Typ.eqb ty ty') && (((x =? x') && (y =? y')) || ((x =? y') && (y =? x')))
           | _, _ => false
         end
       | _, _ => false
@@ -287,12 +287,12 @@ intros. destruct H0; now contradict H0.
     Proof.
       intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H2]]]; rewrite check_diseqs_spec in H2; destruct H2 as [H2 H3]; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl.
       intros l H4; case_eq (distinct (Typ.i_eqb t_i A) (rev l)).
-      rewrite distinct_spec; intro H5; symmetry; apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap by exact Hi; destruct (H2 _ Hi) as [H9 [a [H10 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H10; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H11: a < length t_atom).
-      case_eq (a < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H11; rewrite (get_outofbound _ _ _ H11) in H6; rewrite default_t_atom in H6; inversion H6.
+      rewrite distinct_spec; intro H5; symmetry; apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap by exact Hi; destruct (H2 _ Hi) as [H9 [a [H10 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H10; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H11: a <? length t_atom).
+      case_eq (a <? length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H11; rewrite (get_outofbound _ _ _ H11) in H6; rewrite default_t_atom in H6; inversion H6.
       generalize (wt_t_atom _ H11); rewrite H6; simpl; rewrite !andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h1) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h1) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h2) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) h2) A)); rewrite !Typ.eqb_spec; intros [[_ H13] H12]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h1); rewrite H13; intros [v1 HH1]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h2); rewrite H12; intros [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; simpl; destruct H8 as [H8|H8]; [ |rewrite Typ.i_eqb_sym]; rewrite H5; auto with smtcoq_spl_op smtcoq_core; rewrite H4; [exists h2; exists h1|exists h1; exists h2]; auto with smtcoq_spl_op smtcoq_core.
       rewrite distinct_false_spec; intros [v2 [v1 [H5 H6]]]; rewrite H4 in H5; destruct H5 as [a [b [H5 [H7 H8]]]]; clear H4; change (Typ.i_eqb t_i A v2 v1 = true) with (is_true (Typ.i_eqb t_i A v2 v1)) in H6; rewrite Typ.i_eqb_spec in H6; subst v2; clear H2; destruct (H3 _ _ H5) as [i [H2 [H4 [hb [H6 [H9 H10]]]]]]; clear H3; symmetry; apply (afold_left_andb_false i); rewrite ?length_amap; auto with smtcoq_spl_op smtcoq_core; rewrite get_amap by assumption; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; destruct H10 as [H10|H10]; rewrite H10; simpl; rewrite H7, H8; simpl; rewrite Typ.cast_refl; simpl; replace (Typ.i_eqb t_i A v1 v1) with true; auto with smtcoq_spl_op smtcoq_core; symmetry; change (is_true (Typ.i_eqb t_i A v1 v1)); rewrite Typ.i_eqb_spec; auto with smtcoq_spl_op smtcoq_core.
-      intros [a [H20 H21]]; assert (H4: ha < length t_atom).
-      case_eq (ha < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate.
+      intros [a [H20 H21]]; assert (H4: ha <? length t_atom).
+      case_eq (ha <? length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate.
       unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; generalize (wt_t_atom _ H4); rewrite H1; simpl; rewrite andb_true_iff, forallb_forall; intros [_ H5]; assert (H6 := H5 _ H20); generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a); intros [va Ha]; rewrite Ha in H21; simpl in H21; elim H21; apply Typ.eqb_spec; auto with smtcoq_spl_op smtcoq_core.
     Qed.
 
@@ -300,7 +300,7 @@ intros. destruct H0; now contradict H0.
       check_distinct_two_args f1 f2 = true ->
       rho f1 = negb (rho f2).
     Proof.
-      intros f1 f2; rewrite check_distinct_two_args_spec; intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; unfold Form.interp_state_var; assert (H5: f1 < length t_form) by (case_eq (f1 < length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); assert (H6: f2 < length t_form) by (case_eq (f2 < length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H2; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); rewrite !Form.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H1, H2; simpl; unfold Atom.interp_form_hatom, Atom.interp_hatom; rewrite !Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H3, H4; simpl; unfold Atom.wt,is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H7: hb < length t_atom) by (case_eq (hb < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H4; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate); generalize (wt_t_atom _ H7); rewrite H4; simpl; case (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) hb); try discriminate; simpl; rewrite andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A)); rewrite !Typ.eqb_spec; intros [H8 H9]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom x), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom y); rewrite H8, H9; intros [v1 HH1] [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; auto with smtcoq_spl_op smtcoq_core; rewrite Typ.i_eqb_sym; auto with smtcoq_spl_op smtcoq_core.
+      intros f1 f2; rewrite check_distinct_two_args_spec; intros [ha [hb [A [x [y [H1 [H2 [H3 [H4|H4]]]]]]]]]; unfold Form.interp_state_var; assert (H5: f1 <? length t_form) by (case_eq (f1 <? length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); assert (H6: f2 <? length t_form) by (case_eq (f2 <? length t_form); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H2; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_form; discriminate); rewrite !Form.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H1, H2; simpl; unfold Atom.interp_form_hatom, Atom.interp_hatom; rewrite !Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H3, H4; simpl; unfold Atom.wt,is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H7: hb <? length t_atom) by (case_eq (hb <? length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H4; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate); generalize (wt_t_atom _ H7); rewrite H4; simpl; case (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) hb); try discriminate; simpl; rewrite andb_true_iff; change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) x) A)); change (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A = true) with (is_true (Typ.eqb (Atom.get_type' t_i (Atom.t_interp t_i t_func t_atom) y) A)); rewrite !Typ.eqb_spec; intros [H8 H9]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom x), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom y); rewrite H8, H9; intros [v1 HH1] [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; auto with smtcoq_spl_op smtcoq_core; rewrite Typ.i_eqb_sym; auto with smtcoq_spl_op smtcoq_core.
     Qed.
 
 
@@ -309,11 +309,11 @@ intros. destruct H0; now contradict H0.
     (*   interp_form_hatom ha -> afold_left bool int true andb (Lit.interp rho) diseq. *)
     (* Proof. *)
   (*     intros ha diseq; rewrite check_distinct_spec; intros [A [dist [H1 H]]]; rewrite check_diseqs_spec in H; unfold Atom.interp_form_hatom, Atom.interp_bool, Atom.interp_hatom; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H1; simpl; generalize (Atom.compute_interp_spec_rev t_i (get (Atom.t_interp t_i t_func t_atom)) A dist); case (Atom.compute_interp t_i (get (Atom.t_interp t_i t_func t_atom)) A nil); simpl. *)
-  (*     intros l H2; unfold is_true; rewrite distinct_spec; intro H3; apply afold_left_andb_true; intros i Hi; destruct (H _ Hi) as [H4 [a [H5 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H5; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H10: a < length t_atom). *)
-  (*     case_eq (a < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H10; rewrite (get_outofbound _ _ _ H10) in H6; rewrite default_t_atom in H6; inversion H6. *)
+  (*     intros l H2; unfold is_true; rewrite distinct_spec; intro H3; apply afold_left_andb_true; intros i Hi; destruct (H _ Hi) as [H4 [a [H5 [h1 [h2 [H6 [H7 H8]]]]]]]; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto with smtcoq_spl_op smtcoq_core); unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_spl_op smtcoq_core; rewrite H5; simpl; rewrite Atom.t_interp_wf; auto with smtcoq_spl_op smtcoq_core; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; assert (H10: a <? length t_atom). *)
+  (*     case_eq (a <? length t_atom); auto with smtcoq_spl_op smtcoq_core; intro H10; rewrite (get_outofbound _ _ _ H10) in H6; rewrite default_t_atom in H6; inversion H6. *)
   (*     generalize (wt_t_atom _ H10); rewrite H6; simpl; rewrite !andb_true_iff. change (Typ.eqb (Atom.get_type t_i t_func t_atom h1) A = true) with (is_true (Typ.eqb (Atom.get_type t_i t_func t_atom h1) A)); change (Typ.eqb (Atom.get_type t_i t_func t_atom h2) A = true) with (is_true (Typ.eqb (Atom.get_type t_i t_func t_atom h2) A)); rewrite !Typ.eqb_spec; intros [[_ H11] H12]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h1); rewrite H11; intros [v1 HH1]; generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom h2); rewrite H12; intros [v2 HH2]; rewrite HH1, HH2; simpl; rewrite Typ.cast_refl; simpl; destruct H8 as [H8|H8]; [ |rewrite Typ.i_eqb_sym]; rewrite H3; auto with smtcoq_spl_op smtcoq_core; rewrite H2; [exists h2; exists h1|exists h1; exists h2]; auto with smtcoq_spl_op smtcoq_core. *)
-  (*     intros [a [H2 H3]] _; assert (H4: ha < length t_atom). *)
-  (*     case_eq (ha < length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate. *)
+  (*     intros [a [H2 H3]] _; assert (H4: ha <? length t_atom). *)
+  (*     case_eq (ha <? length t_atom); auto with smtcoq_spl_op smtcoq_core; intro Heq; generalize H1; rewrite get_outofbound; auto with smtcoq_spl_op smtcoq_core; rewrite default_t_atom; discriminate. *)
   (*     unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite aforallbi_spec in wt_t_atom; generalize (wt_t_atom _ H4); rewrite H1; simpl; rewrite andb_true_iff, forallb_forall; intros [_ H5]; assert (H6 := H5 _ H2); generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a); intros [va Ha]; rewrite Ha in H3; simpl in H3; elim H3; apply Typ.eqb_spec; auto with smtcoq_spl_op smtcoq_core. *)
   (*   Qed. *)
 
@@ -325,22 +325,22 @@ intros. destruct H0; now contradict H0.
     Variable check_var : var -> var -> bool.
 
     Definition check_lit l1 l2 :=
-      (l1 == l2) || ((Bool.eqb (Lit.is_pos l1) (Lit.is_pos l2)) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((Bool.eqb (Lit.is_pos l1) (negb (Lit.is_pos l2))) && (check_distinct_two_args (Lit.blit l1) (Lit.blit l2))).
+      (l1 =? l2) || ((Bool.eqb (Lit.is_pos l1) (Lit.is_pos l2)) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((Bool.eqb (Lit.is_pos l1) (negb (Lit.is_pos l2))) && (check_distinct_two_args (Lit.blit l1) (Lit.blit l2))).
 
     (* Definition check_lit l1 l2 := *)
-    (*   (l1 == l2) || ((Lit.is_pos l1) && (Lit.is_pos l2) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((negb (Lit.is_pos l1)) && (negb (Lit.is_pos l2)) && (check_var (Lit.blit l2) (Lit.blit l1))). *)
+    (*   (l1 =? l2) || ((Lit.is_pos l1) && (Lit.is_pos l2) && (check_var (Lit.blit l1) (Lit.blit l2))) || ((negb (Lit.is_pos l1)) && (negb (Lit.is_pos l2)) && (check_var (Lit.blit l2) (Lit.blit l1))). *)
 
     Definition check_form_aux a b :=
       match a, b with
         | Fatom ha, Fand diseq => check_distinct ha diseq
-        | Fatom a, Fatom b => a == b
+        | Fatom a, Fatom b => a =? b
         | Ftrue, Ftrue => true
         | Ffalse, Ffalse => true
-        | Fnot2 i1 l1, Fnot2 i2 l2 => (i1 == i2) && (check_lit l1 l2)
-        | Fand a1, Fand a2 => (length a1 == length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1)
-        | For a1, For a2 => (length a1 == length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1)
-        | Fimp a1, Fimp a2 => (length a1 == length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1)
-          (* (length a1 == length a2) && (aforallbi (fun i l => if i < length a1 - 1 then check_lit (a2.[i]) l else check_lit l (a2.[i])) a1) *)
+        | Fnot2 i1 l1, Fnot2 i2 l2 => (i1 =? i2) && (check_lit l1 l2)
+        | Fand a1, Fand a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1)
+        | For a1, For a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1)
+        | Fimp a1, Fimp a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1)
+          (* (length a1 =? length a2) && (aforallbi (fun i l => if i <? length a1 - 1 then check_lit (a2.[i]) l else check_lit l (a2.[i])) a1) *)
         | Fxor l1 l2, Fxor j1 j2 => check_lit l1 j1 && check_lit l2 j2
           (* check_lit l1 j1 && check_lit j1 l1 && check_lit l2 j2 && check_lit j2 l2 *)
           (* (* let a := check_lit l1 j1 in *) *)
@@ -450,16 +450,16 @@ intros. destruct H0; now contradict H0.
     (*   rewrite <- H1; eauto with smtcoq_core. *)
     (*   eapply interp_check_lit; eauto with smtcoq_core. *)
     (*   (* Implication *) *)
-    (*   unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite aforallbi_spec in H2; intro H3; apply afold_right_implb_true; case_eq (length a1 == 0); intro Heq. *)
+    (*   unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite aforallbi_spec in H2; intro H3; apply afold_right_implb_true; case_eq (length a1 =? 0); intro Heq. *)
     (*   left; rewrite eqb_spec in Heq; rewrite <- H1; auto with smtcoq_core. *)
     (*   destruct (afold_right_implb_true_inv _ _ _ H3) as [H4|[[i [H4 H5]]|H4]]. *)
     (*   rewrite H4 in Heq; discriminate. *)
-    (*   right; left; exists i; rewrite <- H1; split; auto with smtcoq_core; case_eq (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; intro H6; assert (H7: i < length a1 = true). *)
+    (*   right; left; exists i; rewrite <- H1; split; auto with smtcoq_core; case_eq (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; intro H6; assert (H7: i <? length a1 = true). *)
     (*   rewrite ltb_spec in *; rewrite eqb_false_spec in Heq; rewrite to_Z_sub_1_diff in H4; auto with smtcoq_core; omega. *)
     (*   generalize (H2 _ H7); rewrite H4; intro H8; rewrite (interp_check_lit _ _ H8 H6) in H5; auto with smtcoq_core. *)
-    (*   right; case_eq (aexistsbi (fun i l => (i < length a2 - 1) && (negb (Lit.interp rho l))) a2). *)
+    (*   right; case_eq (aexistsbi (fun i l => (i <? length a2 - 1) && (negb (Lit.interp rho l))) a2). *)
     (*   rewrite aexistsbi_spec; intros [i [_ H5]]; rewrite andb_true_iff in H5; destruct H5 as [H5 H6]; left; exists i; split; auto with smtcoq_core; generalize H6; case (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; discriminate. *)
-    (*   rewrite aexistsbi_false_spec; intro H; right; intros i Hi; assert (Hi' := Hi); rewrite <- H1 in Hi'; generalize (H2 _ Hi') (H _ Hi); rewrite <- H1; case (i < length a1 - 1); simpl. *)
+    (*   rewrite aexistsbi_false_spec; intro H; right; intros i Hi; assert (Hi' := Hi); rewrite <- H1 in Hi'; generalize (H2 _ Hi') (H _ Hi); rewrite <- H1; case (i <? length a1 - 1); simpl. *)
     (*   intros _; case (Lit.interp rho (a2 .[ i])); auto with smtcoq_core; discriminate. *)
     (*   intros H5 _; apply (interp_check_lit _ _ H5); apply H4; auto with smtcoq_core. *)
     (*   (* Xor *) *)
@@ -474,7 +474,7 @@ intros. destruct H0; now contradict H0.
 
   Definition check_hform h1 h2 :=
     foldi
-    (fun _ cont h1 h2 => (h1 == h2) || check_form_aux cont (get_form h1) (get_form h2))
+    (fun _ cont h1 h2 => (h1 =? h2) || check_form_aux cont (get_form h1) (get_form h2))
     0 (PArray.length t_form) (fun h1 h2 => false) h1 h2.
 
   Definition check_form := check_form_aux check_hform.
diff --git a/src/spl/Syntactic.v b/src/spl/Syntactic.v
index eb512ee..ea55500 100644
--- a/src/spl/Syntactic.v
+++ b/src/spl/Syntactic.v
@@ -77,7 +77,7 @@ Section CheckAtom.
           match o1, o2 with
             | NO_distinct t1, NO_distinct t2 => Typ.eqb t1 t2 && list_beq check_hatom l1 l2
           end
-        | Aapp f1 aargs, Aapp f2 bargs =>(f1 == f2) && list_beq check_hatom aargs bargs
+        | Aapp f1 aargs, Aapp f2 bargs =>(f1 =? f2) && list_beq check_hatom aargs bargs
 
         | _, _ => false
       end.
@@ -191,7 +191,7 @@ Section CheckAtom.
 
   Definition check_hatom h1 h2 :=
     foldi
-    (fun _ cont h1 h2 => (h1 == h2) || check_atom_aux cont (t_atom.[h1]) (t_atom.[h2]))
+    (fun _ cont h1 h2 => (h1 =? h2) || check_atom_aux cont (t_atom.[h1]) (t_atom.[h2]))
     0 (PArray.length t_atom) (fun h1 h2 => false) h1 h2.
 
   Definition check_atom := check_atom_aux check_hatom.
@@ -269,7 +269,7 @@ Section CheckAtom.
         | Val _ _, Val _ _ => False
       end.
   Proof.
-    unfold wt; unfold is_true at 1; rewrite aforallbi_spec; intros Hwt Hwf Hdef h1 h2; unfold check_neg_hatom; case_eq (get_atom h1); try discriminate; intros b1 t11 t12 H1; case_eq (get_atom h2); try discriminate; intros b2 t21 t22 H2; assert (H7: h1 < length t_atom) by (apply PArray.get_not_default_lt; rewrite H1, Hdef; discriminate); generalize (Hwt _ H7); rewrite H1; simpl; generalize H1; case b1; try discriminate; clear H1 b1; simpl; intro H1; case (get_type' t_i (t_interp t_i t_func t_atom) h1); try discriminate; simpl; rewrite andb_true_iff; intros [H30 H31]; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t11) Typ.TZ)) in H30; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t12) Typ.TZ)) in H31; rewrite Typ.eqb_spec in H30, H31; generalize (check_aux_interp_hatom _ t_func _ Hwf t11), (check_aux_interp_hatom _ t_func _ Hwf t12); rewrite H30, H31; intros [v1 Hv1] [v2 Hv2]; generalize H2; case b2; try discriminate; clear H2 b2; intro H2; unfold is_true; rewrite andb_true_iff; intros [H3 H4]; generalize (check_hatom_correct Hwf Hdef _ _ H3), (check_hatom_correct Hwf Hdef _ _ H4); unfold interp_hatom; intros H5 H6; rewrite t_interp_wf; auto; rewrite H1; simpl; rewrite Hv1, Hv2; simpl; rewrite t_interp_wf; auto; rewrite H2; simpl; rewrite <- H5; rewrite <- H6, Hv1, Hv2; simpl.
+    unfold wt; unfold is_true at 1; rewrite aforallbi_spec; intros Hwt Hwf Hdef h1 h2; unfold check_neg_hatom; case_eq (get_atom h1); try discriminate; intros b1 t11 t12 H1; case_eq (get_atom h2); try discriminate; intros b2 t21 t22 H2; assert (H7: h1 <? length t_atom) by (apply PArray.get_not_default_lt; rewrite H1, Hdef; discriminate); generalize (Hwt _ H7); rewrite H1; simpl; generalize H1; case b1; try discriminate; clear H1 b1; simpl; intro H1; case (get_type' t_i (t_interp t_i t_func t_atom) h1); try discriminate; simpl; rewrite andb_true_iff; intros [H30 H31]; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t11) Typ.TZ)) in H30; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t12) Typ.TZ)) in H31; rewrite Typ.eqb_spec in H30, H31; generalize (check_aux_interp_hatom _ t_func _ Hwf t11), (check_aux_interp_hatom _ t_func _ Hwf t12); rewrite H30, H31; intros [v1 Hv1] [v2 Hv2]; generalize H2; case b2; try discriminate; clear H2 b2; intro H2; unfold is_true; rewrite andb_true_iff; intros [H3 H4]; generalize (check_hatom_correct Hwf Hdef _ _ H3), (check_hatom_correct Hwf Hdef _ _ H4); unfold interp_hatom; intros H5 H6; rewrite t_interp_wf; auto; rewrite H1; simpl; rewrite Hv1, Hv2; simpl; rewrite t_interp_wf; auto; rewrite H2; simpl; rewrite <- H5; rewrite <- H6, Hv1, Hv2; simpl.
     rewrite Z.ltb_antisym; auto.
     rewrite Z.geb_leb, Z.ltb_antisym; auto.
     rewrite Z.leb_antisym; auto.
@@ -354,8 +354,8 @@ Section FLATTEN.
   Definition check_flatten_body frec (l lf:_lit) :=
     let l := remove_not l in
       let lf := remove_not lf in
-        if l == lf then true
-          else if 1 land (l lxor lf) == 0 then
+        if l =? lf then true
+          else if 1 land (l lxor lf) =? 0 then
             match get_form (Lit.blit l), get_form (Lit.blit lf) with
               | Fatom a1, Fatom a2 => check_atom a1 a2
               | Ftrue, Ftrue => true
@@ -371,7 +371,7 @@ Section FLATTEN.
               | Fxor l1 l2, Fxor lf1 lf2 =>
                 frec l1 lf1 && frec l2 lf2
               | Fimp args1, Fimp args2 =>
-                if PArray.length args1 == PArray.length args2 then
+                if PArray.length args1 =? PArray.length args2 then
                   aforallbi (fun i l => frec l (args2.[i])) args1
                   else false
               | Fiff l1 l2, Fiff lf1 lf2 =>