Hints in databases

12 files changed, 481 insertions, 506 deletions

diff --git a/src/Misc.v b/src/Misc.v
index b675599..952985f 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -763,26 +763,26 @@ Section List2.
   | In2_hd : forall l, In j l -> In2 i j (i::l)
   | In2_tl : forall k l, In2 i j l -> In2 i j (k::l).
 
-  Local Hint Constructors In2.
+  Local Hint Constructors In2 : smtcoq_in2.
 
 
   Lemma In2_app : forall i j l m, In2 i j (l ++ m) <->
     In2 i j l \/ (In i l /\ In j m) \/ In2 i j m.
   Proof.
-    intros i j; induction l as [ |t l IHl]; simpl; intro m; split; auto.
-    intros [H|[[H _]|H]]; auto.
+    intros i j; induction l as [ |t l IHl]; simpl; intro m; split; auto with smtcoq_in2.
+    intros [H|[[H _]|H]]; auto with smtcoq_in2.
     inversion H.
     elim H.
     intro H; inversion H; clear H.
-    subst i l0; rewrite in_app_iff in H1; destruct H1 as [H1|H1]; auto.
-    subst k l0; rewrite IHl in H1; destruct H1 as [H1|[[H1 H2]|H1]]; auto.
+    subst i l0; rewrite in_app_iff in H1; destruct H1 as [H1|H1]; auto with smtcoq_in2.
+    subst k l0; rewrite IHl in H1; destruct H1 as [H1|[[H1 H2]|H1]]; auto with smtcoq_in2.
     intros [H|[[[H|H] H1]|H]].
     inversion H; clear H.
-    subst i l0; constructor 1; rewrite in_app_iff; auto.
-    subst k l0; constructor 2; rewrite IHl; left; auto.
-    subst t; constructor 1; rewrite in_app_iff; auto.
-    constructor 2; rewrite IHl; right; left; auto.
-    constructor 2; rewrite IHl; right; right; auto.
+    subst i l0; constructor 1; rewrite in_app_iff; auto with smtcoq_in2.
+    subst k l0; constructor 2; rewrite IHl; left; auto with smtcoq_in2.
+    subst t; constructor 1; rewrite in_app_iff; auto with smtcoq_in2.
+    constructor 2; rewrite IHl; right; left; auto with smtcoq_in2.
+    constructor 2; rewrite IHl; right; right; auto with smtcoq_in2.
   Qed.
 
 
@@ -796,17 +796,17 @@ Section List2.
   Lemma In2_rev_aux : forall i j l acc, In2 i j (rev_aux acc l) <->
     In2 i j acc \/ (In i l /\ In j acc) \/ In2 j i l.
   Proof.
-    intros i j; induction l as [ |t q IHq]; simpl; intro acc; split; auto.
-    intros [H|[[H _]|H]]; auto.
+    intros i j; induction l as [ |t q IHq]; simpl; intro acc; split; auto with smtcoq_in2.
+    intros [H|[[H _]|H]]; auto with smtcoq_in2.
     elim H.
     inversion H.
-    rewrite IHq; clear IHq; intros [H|[[H1 H2]|H]]; auto.
-    inversion H; auto.
-    inversion H2; auto; clear H2; subst t; right; right; auto.
-    intros [H|[[[H1|H1] H2]|H]]; rewrite IHq; clear IHq; auto.
-    subst t; auto.
-    right; left; split; auto; constructor 2; auto.
-    inversion H; clear H; auto; subst j l; right; left; split; auto; constructor 1; auto.
+    rewrite IHq; clear IHq; intros [H|[[H1 H2]|H]]; auto with smtcoq_in2.
+    inversion H; auto with smtcoq_in2.
+    inversion H2; auto with smtcoq_in2; clear H2; subst t; right; right; auto with smtcoq_in2.
+    intros [H|[[[H1|H1] H2]|H]]; rewrite IHq; clear IHq; auto with smtcoq_in2.
+    subst t; auto with smtcoq_in2.
+    right; left; split; auto with smtcoq_in2; constructor 2; auto with smtcoq_in2.
+    inversion H; clear H; auto with smtcoq_in2; subst j l; right; left; split; auto with smtcoq_in2; constructor 1; auto with smtcoq_in2.
   Qed.
 
 
@@ -815,7 +815,7 @@ Section List2.
 
   Lemma In2_rev : forall i j l, In2 i j (rev l) <-> In2 j i l.
   Proof.
-    intros i j l; unfold rev; rewrite In2_rev_aux; split; auto; intros [H|[[_ H]|H]]; auto; inversion H.
+    intros i j l; unfold rev; rewrite In2_rev_aux; split; auto with smtcoq_in2; intros [H|[[_ H]|H]]; auto with smtcoq_in2; inversion H.
   Qed.
 
 
@@ -825,15 +825,15 @@ Section List2.
     intros [H1 H2]; generalize H1 H2; clear H1 H2; induction l as [ |t q IHq].
     intro H1; inversion H1.
     intros H1 H2; inversion H1; clear H1.
-    subst t; inversion H2; auto; elim H; auto.
+    subst t; inversion H2; auto with smtcoq_in2; elim H; auto with smtcoq_in2.
     inversion H2; clear H2.
-    subst t; auto.
-    destruct (IHq H0 H1) as [H2|H2]; auto.
+    subst t; auto with smtcoq_in2.
+    destruct (IHq H0 H1) as [H2|H2]; auto with smtcoq_in2.
     intros [H1|H1]; induction H1 as [H1|t q H1 [IH1 IH2]].
-    split; [constructor 1|constructor 2]; auto.
-    split; constructor 2; auto.
-    split; [constructor 2|constructor 1]; auto.
-    split; constructor 2; auto.
+    split; [constructor 1|constructor 2]; auto with smtcoq_in2.
+    split; constructor 2; auto with smtcoq_in2.
+    split; [constructor 2|constructor 1]; auto with smtcoq_in2.
+    split; constructor 2; auto with smtcoq_in2.
   Qed.
 
 End List2.
@@ -892,32 +892,32 @@ Section Distinct.
         distinct_aux acc' q
     end.
 
-  Local Hint Constructors In2.
+  Local Hint Constructors In2 : smtcoq_in2.
 
   Lemma distinct_aux_spec : forall l acc, distinct_aux acc l = true <->
     acc = true /\ (forall i j, In2 i j l -> eq i j = false).
   Proof.
     induction l as [ |t q IHq]; simpl.
     intro acc; split.
-    intro H; split; auto; intros i j H1; inversion H1.
-    intros [H _]; auto.
+    intro H; split; auto with smtcoq_in2; intros i j H1; inversion H1.
+    intros [H _]; auto with smtcoq_in2.
     intro acc; rewrite (IHq (distinct_aux2 acc t q)), distinct_aux2_spec; split.
-    intros [[H1 H2] H3]; split; auto; intros i j H; inversion H; auto.
-    intros [H1 H2]; repeat split; auto.
+    intros [[H1 H2] H3]; split; auto with smtcoq_in2; intros i j H; inversion H; auto with smtcoq_in2.
+    intros [H1 H2]; repeat split; auto with smtcoq_in2.
   Qed.
 
   Lemma distinct_aux_spec_neg : forall l acc, distinct_aux acc l = false <->
     acc = false \/ (exists i j, In2 i j l /\ eq i j = true).
   Proof.
     induction l as [ |t q IHq]; simpl.
-    intro acc; split; auto; intros [H|[i [j [H _]]]]; auto; inversion H.
+    intro acc; split; auto with smtcoq_in2; intros [H|[i [j [H _]]]]; auto with smtcoq_in2; inversion H.
     intro acc; rewrite (IHq (distinct_aux2 acc t q)), distinct_aux2_spec_neg; split.
-    intros [[H|[i [H1 H2]]]|[i [j [H1 H2]]]]; auto.
-    right; exists t; exists i; auto.
-    right; exists i; exists j; auto.
-    intros [H|[i [j [H1 H2]]]]; auto; inversion H1; clear H1.
-    subst i l; left; right; exists j; auto.
-    subst k l; right; exists i; exists j; auto.
+    intros [[H|[i [H1 H2]]]|[i [j [H1 H2]]]]; auto with smtcoq_in2.
+    right; exists t; exists i; auto with smtcoq_in2.
+    right; exists i; exists j; auto with smtcoq_in2.
+    intros [H|[i [j [H1 H2]]]]; auto with smtcoq_in2; inversion H1; clear H1.
+    subst i l; left; right; exists j; auto with smtcoq_in2.
+    subst k l; right; exists i; exists j; auto with smtcoq_in2.
   Qed.
 
   Definition distinct := distinct_aux true.
@@ -925,13 +925,13 @@ Section Distinct.
   Lemma distinct_spec : forall l, distinct l = true <->
     (forall i j, In2 i j l -> eq i j = false).
   Proof.
-    unfold distinct; intro l; rewrite distinct_aux_spec; split; auto; intros [_ H]; auto.
+    unfold distinct; intro l; rewrite distinct_aux_spec; split; auto with smtcoq_in2; intros [_ H]; auto with smtcoq_in2.
   Qed.
 
   Lemma distinct_false_spec : forall l, distinct l = false <->
     (exists i j, In2 i j l /\ eq i j = true).
   Proof.
-    unfold distinct; intro l; rewrite distinct_aux_spec_neg; split; auto; intros [H|H]; auto; discriminate.
+    unfold distinct; intro l; rewrite distinct_aux_spec_neg; split; auto with smtcoq_in2; intros [H|H]; auto with smtcoq_in2; discriminate.
   Qed.
 
 End Distinct.
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index a85804c..1df1ab7 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -18,7 +18,7 @@ Local Open Scope list_scope.
 Local Open Scope array_scope.
 Local Open Scope int63_scope.
 
-Hint Unfold is_true.
+Hint Unfold is_true : smtcoq_core.
 
 
 (* Remark: I use Notation instead of Definition du eliminate conversion check during the type checking *)
@@ -125,11 +125,11 @@ Module Form.
         destruct h;simpl;intros;trivial;
           try (apply afold_left_eq;unfold is_true in H0;
             rewrite PArray.forallb_spec in H0;intros;
-              auto using Lit.interp_eq_compat).
+              auto using Lit.interp_eq_compat with smtcoq_core).
         - f_equal;auto using Lit.interp_eq_compat.
         - apply afold_right_eq;unfold is_true in H0;
             rewrite PArray.forallb_spec in H0;intros;
-              auto using Lit.interp_eq_compat.
+              auto using Lit.interp_eq_compat with smtcoq_core.
         - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0;
             rewrite !(Lit.interp_eq_compat f1 f2);auto.
         - unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0;
@@ -138,7 +138,7 @@ Module Form.
             rewrite !(Lit.interp_eq_compat f1 f2);auto.
         - replace (List.map (Lit.interp f2) l) with (List.map (Lit.interp f1) l); auto.
           unfold is_true in H0. rewrite List.forallb_forall in H0.
-          apply List_map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto.
+          apply List_map_ext_in. intros x Hx. apply Lit.interp_eq_compat; auto with smtcoq_core.
       Qed.
 
       Definition wf := PArray.forallbi lt_form t_form.
@@ -589,11 +589,11 @@ Module Typ.
     (* TODO : Move this *)
     Lemma not_false : ~ false.
     Proof. intro;discriminate. Qed.
-    Hint Resolve not_false.
+    Hint Resolve not_false : smtcoq_core.
 
     Lemma is_true_true : true.
     Proof. reflexivity. Qed.
-    Hint Resolve is_true_true.
+    Hint Resolve is_true_true : smtcoq_core.
 
     Lemma not_is_true_eq_false : forall b:bool, ~ b <-> b = false.
     Proof. exact not_true_iff_false. Qed.
@@ -1231,8 +1231,8 @@ Qed.
         intros [op|op h|op h1 h2|op ha i i0|f args | i e ]; simpl.
         (* Constants *)
         left; destruct op; simpl.
-        exists Typ.Tpositive; auto.
-        exists Typ.TZ; auto.
+        exists Typ.Tpositive; auto with smtcoq_core.
+        exists Typ.TZ; auto with smtcoq_core.
         exists (Typ.TBV n); now rewrite N.eqb_refl.
         (* Unary operators *)
         destruct op; simpl;
@@ -1440,7 +1440,7 @@ Qed.
           right. intros. rewrite andb_false_r. easy.
         (* N-ary operators *)
         destruct f as [ty]; simpl; case (List.forallb (fun t1 : int => Typ.eqb (get_type t1) ty) args).
-        left; exists Typ.Tbool; auto.
+        left; exists Typ.Tbool; auto with smtcoq_core.
         right; intro T; rewrite andb_false_r; auto.
         (* Application *)
         case (v_type Typ.ftype interp_ft (t_func .[ i])); intros; apply check_args_dec.
diff --git a/src/Trace.v b/src/Trace.v
index e7c7d22..86250a2 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -280,7 +280,7 @@ Module Cnf_Checker.
     checker_b t_form l b c = true ->
     Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l = b.
  Proof.
-   unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto; rewrite Lit.interp_neg, H1; auto.
+   unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto with smtcoq_core; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto with smtcoq_core; rewrite Lit.interp_neg, H1; auto with smtcoq_core.
  Qed.
 
  Definition checker_eq t_form l1 l2 l (c:certif) :=
@@ -297,8 +297,8 @@ Module Cnf_Checker.
     Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2.
  Proof.
    unfold checker_eq; intros t_var t_form l1 l2 l c; rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form).
-   unfold checker in H3; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) _ H3) as [[Ht1 Ht2] Ht3]; split; auto.
-   destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2); intro Heq2; auto; elim (checker_correct H3 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto.
+   unfold checker in H3; destruct c as (nclauses, t, confl); rewrite andb_true_iff in H3; destruct H3 as [H3 _]; destruct (Form.check_form_correct (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) _ H3) as [[Ht1 Ht2] Ht3]; split; auto with smtcoq_core.
+   destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l2); intro Heq2; auto with smtcoq_core; elim (checker_correct H3 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_core; rewrite Heq; simpl; rewrite Heq1, Heq2; auto with smtcoq_core.
  Qed.
 
 End Cnf_Checker.
@@ -433,49 +433,49 @@ Inductive step :=
     |pos orig1 orig2 res|pos orig1 orig2 res
     |pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res
     |pos cl |pos orig res |pos orig res |pos orig res | pos orig1 orig2 res | pos orig1 orig2 res |pos res|pos res
-    |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto.
-    - apply S.valid_set_resolve; auto.
-    - apply S.valid_set_weaken; auto.
-    - apply valid_check_flatten; auto; intros h1 h2 H.
-      + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto.
-      + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto.
-    - apply valid_check_True; auto.
-    - apply valid_check_False; auto.
-    - apply valid_check_BuildDef; auto.
-    - apply valid_check_BuildDef2; auto.
-    - apply valid_check_BuildProj; auto.
-    - apply valid_check_ImmBuildDef; auto.
-    - apply valid_check_ImmBuildDef2; auto.
-    - apply valid_check_ImmBuildProj; auto.
-    - apply valid_check_trans; auto.
-    - apply valid_check_congr; auto.
-    - apply valid_check_congr_pred; auto.
-    - apply valid_check_micromega; auto.
-    - apply valid_check_diseq; auto.
-    - apply valid_check_spl_arith; auto.
-    - apply valid_check_distinct_elim; auto.
-    - eapply valid_check_bbVar; eauto.
-    - apply valid_check_bbConst; auto.
-    - apply valid_check_bbOp; auto.
-    - apply valid_check_bbNot; auto.
-    - apply valid_check_bbNeg; auto.
-    - apply valid_check_bbAdd; auto.
-    - apply valid_check_bbConcat; auto.
-    - apply valid_check_bbMult; auto.
-    - apply valid_check_bbUlt; auto.
-    - apply valid_check_bbSlt; auto.
-    - apply valid_check_bbEq; auto.
-    - apply valid_check_bbDiseq; auto.
-    - apply valid_check_bbExtract; auto.
-    - apply valid_check_bbZextend; auto.
-    - apply valid_check_bbSextend; auto.
-    - apply valid_check_bbShl; auto.
-    - apply valid_check_bbShr; auto.
-    - apply valid_check_roweq; auto.
-    - apply valid_check_rowneq; auto.
-    - apply valid_check_ext; auto.
-    - apply valid_check_hole; auto.
-    - apply valid_check_forall_inst with lemma; auto.
+    |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto with smtcoq_core.
+    - apply S.valid_set_resolve; auto with smtcoq_core.
+    - apply S.valid_set_weaken; auto with smtcoq_core.
+    - apply valid_check_flatten; auto with smtcoq_core; intros h1 h2 H.
+      + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto with smtcoq_core.
+      + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto with smtcoq_core.
+    - apply valid_check_True; auto with smtcoq_core.
+    - apply valid_check_False; auto with smtcoq_core.
+    - apply valid_check_BuildDef; auto with smtcoq_core.
+    - apply valid_check_BuildDef2; auto with smtcoq_core.
+    - apply valid_check_BuildProj; auto with smtcoq_core.
+    - apply valid_check_ImmBuildDef; auto with smtcoq_core.
+    - apply valid_check_ImmBuildDef2; auto with smtcoq_core.
+    - apply valid_check_ImmBuildProj; auto with smtcoq_core.
+    - apply valid_check_trans; auto with smtcoq_core.
+    - apply valid_check_congr; auto with smtcoq_core.
+    - apply valid_check_congr_pred; auto with smtcoq_core.
+    - apply valid_check_micromega; auto with smtcoq_core.
+    - apply valid_check_diseq; auto with smtcoq_core.
+    - apply valid_check_spl_arith; auto with smtcoq_core.
+    - apply valid_check_distinct_elim; auto with smtcoq_core.
+    - eapply valid_check_bbVar; eauto with smtcoq_core.
+    - apply valid_check_bbConst; auto with smtcoq_core.
+    - apply valid_check_bbOp; auto with smtcoq_core.
+    - apply valid_check_bbNot; auto with smtcoq_core.
+    - apply valid_check_bbNeg; auto with smtcoq_core.
+    - apply valid_check_bbAdd; auto with smtcoq_core.
+    - apply valid_check_bbConcat; auto with smtcoq_core.
+    - apply valid_check_bbMult; auto with smtcoq_core.
+    - apply valid_check_bbUlt; auto with smtcoq_core.
+    - apply valid_check_bbSlt; auto with smtcoq_core.
+    - apply valid_check_bbEq; auto with smtcoq_core.
+    - apply valid_check_bbDiseq; auto with smtcoq_core.
+    - apply valid_check_bbExtract; auto with smtcoq_core.
+    - apply valid_check_bbZextend; auto with smtcoq_core.
+    - apply valid_check_bbSextend; auto with smtcoq_core.
+    - apply valid_check_bbShl; auto with smtcoq_core.
+    - apply valid_check_bbShr; auto with smtcoq_core.
+    - apply valid_check_roweq; auto with smtcoq_core.
+    - apply valid_check_rowneq; auto with smtcoq_core.
+    - apply valid_check_ext; auto with smtcoq_core.
+    - apply valid_check_hole; auto with smtcoq_core.
+    - apply valid_check_forall_inst with lemma; auto with smtcoq_core.
   Qed.
 
   Definition euf_checker (* t_atom t_form *) s t :=
@@ -490,8 +490,8 @@ Inductive step :=
         ~ (S.valid rho s).
   Proof.
     unfold euf_checker; intros (* t_i t_func t_atom t_form *) rho H1 H2 H10; apply _checker__correct.
-    intros c H; apply C.is_false_correct; auto.
-    apply step_checker_correct; auto.
+    intros c H; apply C.is_false_correct; auto with smtcoq_core.
+    apply step_checker_correct; auto with smtcoq_core.
   Qed.
 
   Inductive certif :=
@@ -516,11 +516,11 @@ Inductive step :=
       forall s d used_roots, S.valid rho s -> valid t_func t_atom t_form d ->
         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); case used_roots.
-    intro ur; apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; case_eq (ur .[ i] < length d).
-    intro; unfold C.valid; simpl; rewrite H5; auto.
-    intros; apply C.interp_true; auto.
-    apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto; intros a i H6 Ha; apply S.valid_set_clause; auto; unfold C.valid; simpl; rewrite H5; auto.
+    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_right_Ind _ _ (fun _ a => S.valid rho a)); auto with smtcoq_core; intros a i H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; case_eq (ur .[ i] < length d).
+    intro; unfold C.valid; simpl; rewrite H5; auto with smtcoq_core.
+    intros; apply C.interp_true; auto with smtcoq_core.
+    apply (foldi_right_Ind _ _ (fun _ a => S.valid rho a)); auto with smtcoq_core; intros a i H6 Ha; apply S.valid_set_clause; auto with smtcoq_core; unfold C.valid; simpl; rewrite H5; auto with smtcoq_core.
   Qed.
 
   Definition checker (* t_i t_func t_atom t_form *) d used_roots (c:certif) :=
@@ -711,7 +711,7 @@ Inductive step :=
     checker (* t_i t_func t_atom t_form *) d used_roots c = true ->
     ~ (valid t_func t_atom t_form d).
   Proof.
-    unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; 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 [_ H4]; auto.
+    unfold checker; intros (* t_i t_func t_atom t_form *) d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[[H1 H2] H10] H3] H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; 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 [_ H4]; auto with smtcoq_core.
   Qed.
 
   Definition checker_b (* t_i t_func t_atom t_form *) l (b:bool) (c:certif) :=
@@ -723,7 +723,7 @@ Inductive step :=
     checker_b (* t_func t_atom t_form *) l b c = true ->
     Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l = b.
   Proof.
-   unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l); auto; intros H1; elim (checker_correct H2); auto; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto; rewrite Lit.interp_neg, H1; auto.
+   unfold checker_b; intros (* t_i t_func t_atom t_form *) l b (nclauses, t, confl); case b; intros H2; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l); auto with smtcoq_core; intros H1; elim (checker_correct H2); auto with smtcoq_core; unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; auto with smtcoq_core; rewrite Lit.interp_neg, H1; auto with smtcoq_core.
  Qed.
 
   Definition checker_eq (* t_i t_func t_atom t_form *) l1 l2 l (c:certif) :=
@@ -741,8 +741,8 @@ Inductive step :=
     Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2.
   Proof.
    unfold checker_eq; intros (* t_i t_func t_atom t_form *) l1 l2 l (nclauses, t, confl); rewrite !andb_true_iff; case_eq (t_form .[ Lit.blit l]); [intros _ _|intros _|intros _|intros _ _ _|intros _ _|intros _ _|intros _ _|intros _ _ _|intros l1' l2' Heq|intros _ _ _ _|intros a ls Heq]; intros [[H1 H2] H3]; try discriminate; rewrite andb_true_iff in H2; rewrite !Int63Properties.eqb_spec in H2; destruct H2 as [H2 H4]; subst l1' l2'; case_eq (Lit.is_pos l); intro Heq'; rewrite Heq' in H1; try discriminate; clear H1; assert (H:PArray.default t_form = Form.Ftrue /\ Form.wf t_form).
-   unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; 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) _ H3) as [[Ht1 Ht2] Ht3]; split; auto.
-   destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2); intro Heq2; auto; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite Heq; simpl; rewrite Heq1, Heq2; auto.
+   unfold checker in H3; rewrite !andb_true_iff in H3; destruct H3 as [[[H3 _] _] _]; 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) _ H3) as [[Ht1 Ht2] Ht3]; split; auto with smtcoq_core.
+   destruct H as [H1 H2]; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l1); intro Heq1; case_eq (Lit.interp (Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form) l2); intro Heq2; auto with smtcoq_core; elim (checker_correct H3); unfold valid; apply afold_left_andb_true; intros i Hi; rewrite get_make; unfold Lit.interp; rewrite Heq'; unfold Var.interp; rewrite Form.wf_interp_form; auto with smtcoq_core; rewrite Heq; simpl; rewrite Heq1, Heq2; auto with smtcoq_core.
  Qed.
 
 
@@ -762,7 +762,7 @@ Inductive step :=
     forall t_i t_func, Atom.wt t_i t_func t_atom ->
                        ~ valid t_func t_atom t_form d.
   Proof.
-    unfold checker_ext; intros t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[H1 H2] H3]; intros t_i t_func H10 H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto.
+    unfold checker_ext; intros t_atom t_form d used_roots (nclauses, t, confl); rewrite !andb_true_iff; intros [[H1 H2] H3]; intros t_i t_func H10 H; eelim euf_checker_correct; try eassumption; apply add_roots_correct; try eassumption; apply S.valid_make; destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) _ H1) as [_ H4]; auto with smtcoq_core.
   Qed.
   *)
 
diff --git a/src/array/FArray.v b/src/array/FArray.v
index a17817f..8048e60 100644
--- a/src/array/FArray.v
+++ b/src/array/FArray.v
@@ -44,7 +44,7 @@ Module Raw.
   Lemma eqb_elt_eq x y : eqb_elt x y = true <-> x = y.
   Proof. unfold eqb_elt. case (eq_dec x y); split; easy. Qed.
 
-  Hint Immediate eqb_key_eq eqb_elt_eq.
+  Hint Immediate eqb_key_eq eqb_elt_eq : smtcoq_array.
 
   Definition farray := list (key * elt).
 
@@ -57,8 +57,8 @@ Module Raw.
   (* Definition ltke (a b : (key * elt)) := *)
   (*   lt (fst a) (fst b) \/ ( (fst a) = (fst b) /\ lt (snd a) (snd b)). *)
 
-  Hint Unfold ltk (* ltke *) eqk eqke.
-  Hint Extern 2 (eqke ?a ?b) => split.
+  Hint Unfold ltk (* ltke *) eqk eqke : smtcoq_array.
+  Hint Extern 2 (eqke ?a ?b) => split : smtcoq_array.
 
   Global Instance lt_key_strorder : StrictOrder (lt : key -> key -> Prop).
   Proof. apply StrictOrder_OrdType. Qed.
@@ -95,7 +95,7 @@ Module Raw.
 
    Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
    Proof. auto. Qed.
-   Hint Immediate ltk_right_r ltk_right_l.
+   Hint Immediate ltk_right_r ltk_right_l : smtcoq_array.
 
   Notation Sort := (sort ltk).
   Notation Inf := (lelistA (ltk)).
@@ -105,7 +105,7 @@ Module Raw.
 
   Notation NoDupA := (NoDupA eqk).
 
-  Hint Unfold MapsTo In.
+  Hint Unfold MapsTo In : smtcoq_array.
 
   (* Instance ke_ord: OrdType (key * elt). *)
   (* Proof. *)
@@ -154,52 +154,52 @@ Module Raw.
   (* eqk, eqke are equalities *)
 
   Lemma eqk_refl : forall e, eqk e e.
-  Proof. auto. Qed.
+  Proof. auto with smtcoq_array. Qed.
 
   Lemma eqke_refl : forall e, eqke e e.
-  Proof. auto. Qed.
+  Proof. auto with smtcoq_array. Qed.
 
   Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.
-  Proof. auto. Qed.
+  Proof. auto with smtcoq_array. Qed.
 
   Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.
   Proof. unfold eqke; intuition. Qed.
 
   Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
-  Proof. eauto. Qed.
+  Proof. eauto with smtcoq_array. Qed.
 
   Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
   Proof.
-    unfold eqke; intuition; [ eauto | congruence ].
+    unfold eqke; intuition; [ eauto with smtcoq_array | congruence ].
   Qed.
 
   Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''.
-  Proof. eauto. Qed.
+  Proof. eauto with smtcoq_array. Qed.
 
   Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
-  Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto. Qed.
+  Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto with smtcoq_array. Qed.
 
   Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
   Proof.
     unfold eqke, ltk; intuition; simpl in *; subst.
-    apply lt_not_eq in H. auto.
+    apply lt_not_eq in H. auto with smtcoq_array.
   Qed.
 
-  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
-  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
-  Hint Immediate eqk_sym eqke_sym.
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : smtcoq_array.
+  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : smtcoq_array.
+  Hint Immediate eqk_sym eqke_sym : smtcoq_array.
 
   Global Instance eqk_equiv : Equivalence eqk.
-  Proof. split; eauto. Qed.
+  Proof. split; eauto with smtcoq_array. Qed.
 
   Global Instance eqke_equiv : Equivalence eqke.
-  Proof. split; eauto. Qed.
+  Proof. split; eauto with smtcoq_array. Qed.
 
   Global Instance ltk_strorder : StrictOrder ltk.
   Proof.
     split.
     unfold Irreflexive, Reflexive, complement.
-    intros. apply lt_not_eq in H; auto.
+    intros. apply lt_not_eq in H; auto with smtcoq_array.
     unfold Transitive. intros x y z. apply lt_trans.
   Qed.
 
@@ -207,13 +207,13 @@ Module Raw.
   (* Proof. *)
   (*   split. *)
   (*   unfold Irreflexive, Reflexive, complement. *)
-  (*   intros. apply lt_not_eq in H; auto. *)
+  (*   intros. apply lt_not_eq in H; auto with smtcoq_array. *)
   (*   unfold Transitive. apply lt_trans. *)
   (* Qed. *)
 
   Global Instance eq_equiv : @Equivalence (key * elt) eq.
   Proof.
-    split; auto.
+    split; auto with smtcoq_array.
     unfold Transitive. apply eq_trans.
   Qed.
 
@@ -230,13 +230,13 @@ Module Raw.
   Global Instance ltk_compatk : Proper (eqk==>eqk==>iff) ltk.
   Proof.
   intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute.
-   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto with smtcoq_array.
   Qed.
 
   Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk.
   Proof.
   intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute.
-   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto with smtcoq_array.
   Qed.
 
   Global Instance ltk_asym : Asymmetric ltk.
@@ -251,8 +251,8 @@ Module Raw.
     destruct x, x'. simpl in *.
     intro.
     symmetry in H.
-    apply lt_not_eq in H. auto.
-    subst. auto.
+    apply lt_not_eq in H. auto with smtcoq_array.
+    subst. auto with smtcoq_array.
   Qed.
 
   Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''.
@@ -265,8 +265,8 @@ Module Raw.
     intros (k,e) (k',e') (k'',e'').
     unfold ltk, eqk; simpl; intros; subst; trivial.
   Qed.
-  Hint Resolve eqk_not_ltk.
-  Hint Immediate ltk_eqk eqk_ltk.
+  Hint Resolve eqk_not_ltk : smtcoq_array.
+  Hint Immediate ltk_eqk eqk_ltk : smtcoq_array.
   
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
@@ -274,19 +274,19 @@ Module Raw.
     unfold eqke; induction 1; intuition.
   Qed.
 
-  Hint Resolve InA_eqke_eqk.
+  Hint Resolve InA_eqke_eqk : smtcoq_array.
 
   (* Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. *)
   (* Proof. *)
-  (*  intros; apply InA_eqA with p; auto with *. *)
+  (*  intros; apply InA_eqA with p; auto with smtcoq_array with *. *)
   (* Qed. *)
 
   (* Lemma In_eq : forall l x y, eq x y -> InA eqke x l -> InA eqke y l. *)
-  (* Proof. intros. rewrite <- H; auto. Qed. *)
+  (* Proof. intros. rewrite <- H; auto with smtcoq_array. Qed. *)
 
   (* Lemma ListIn_In : forall l x, List.In x l -> InA eqk x l. *)
-  (* Proof. apply In_InA. split; auto. unfold Transitive. *)
-  (*   unfold eqk; intros. rewrite H, <- H0. auto. *)
+  (* Proof. apply In_InA. split; auto with smtcoq_array. unfold Transitive. *)
+  (*   unfold eqk; intros. rewrite H, <- H0. auto with smtcoq_array. *)
   (* Qed. *)
   
   (* Lemma Inf_lt : forall l x y, ltk x y -> Inf y l -> Inf x l. *)
@@ -300,12 +300,12 @@ Module Raw.
   Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
   Proof.
   firstorder.
-  exists x; auto.
+  exists x; auto with smtcoq_array.
   induction H.
   destruct y.
-  exists e; auto.
+  exists e; auto with smtcoq_array.
   destruct IHInA as [e H0].
-  exists e; auto.
+  exists e; auto with smtcoq_array.
   Qed.
 
   Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
@@ -315,7 +315,7 @@ Module Raw.
 
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
   Proof.
-  destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
+  destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto with smtcoq_array.
   Qed.
 
   Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
@@ -324,8 +324,8 @@ Module Raw.
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
   Proof. exact (InfA_ltA ltk_strorder). Qed.
 
-  Hint Immediate Inf_eq.
-  Hint Resolve Inf_lt.
+  Hint Immediate Inf_eq : smtcoq_array.
+  Hint Resolve Inf_lt : smtcoq_array.
 
   Lemma Sort_Inf_In :
     forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
@@ -339,11 +339,11 @@ Module Raw.
     intros; red; intros.
     destruct H1 as [e' H2].
     elim (@ltk_not_eqk (k,e) (k,e')).
-    eapply Sort_Inf_In; eauto.
-    red; simpl; auto.
+    eapply Sort_Inf_In; eauto with smtcoq_array.
+    red; simpl; auto with smtcoq_array.
   Qed.
 
-  Hint Resolve Sort_Inf_NotIn.
+  Hint Resolve Sort_Inf_NotIn : smtcoq_array.
 
   Lemma Sort_NoDupA: forall l, Sort l -> NoDupA l.
   Proof.
@@ -352,14 +352,14 @@ Module Raw.
 
   Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
   Proof.
-    inversion 1; intros; eapply Sort_Inf_In; eauto.
+    inversion 1; intros; eapply Sort_Inf_In; eauto with smtcoq_array.
   Qed.
 
   Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
                                    ltk e e' \/ eqk e e'.
   Proof.
-    inversion_clear 2; auto.
-    left; apply Sort_In_cons_1 with l; auto.
+    inversion_clear 2; auto with smtcoq_array.
+    left; apply Sort_In_cons_1 with l; auto with smtcoq_array.
   Qed.
 
   Lemma Sort_In_cons_3 :
@@ -372,7 +372,7 @@ Module Raw.
   Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
   Proof.
     inversion 1.
-    inversion_clear H0; eauto.
+    inversion_clear H0; eauto with smtcoq_array.
     destruct H1; simpl in *; intuition.
   Qed.
 
@@ -388,7 +388,7 @@ Module Raw.
     inversion_clear 1; compute in H0; intuition.
   Qed.
 
-  Hint Resolve In_inv_2 In_inv_3.
+  Hint Resolve In_inv_2 In_inv_3 : smtcoq_array.
 
   (** * FMAPLIST interface implementaion  *)
 
@@ -405,11 +405,11 @@ Module Raw.
     intro abs.
     inversion abs.
   Qed.
-  Hint Resolve empty_1.
+  Hint Resolve empty_1 : smtcoq_array.
 
   Lemma empty_sorted : Sort empty.
   Proof.
-    unfold empty; auto.
+    unfold empty; auto with smtcoq_array.
   Qed.
 
   Lemma MapsTo_inj : forall x e e' l (Hl:Sort l),
@@ -441,7 +441,7 @@ Module Raw.
       + unfold eqk in H, H0. simpl in *. subst.
         inversion_clear HH.
         inversion_clear HH0.
-        unfold eqke in *. simpl in *. destruct H, H1; subst; auto.
+        unfold eqke in *. simpl in *. destruct H, H1; subst; auto with smtcoq_array.
         apply InA_eqke_eqk in H1.
         inversion_clear Hl.
         specialize (Sort_Inf_In H2 H3 H1).
@@ -460,15 +460,15 @@ Module Raw.
   Proof.
     unfold Empty, MapsTo.
     intros m.
-    case m;auto.
+    case m;auto with smtcoq_array.
     intros (k,e) l inlist.
-    absurd (InA eqke (k, e) ((k, e) :: l));auto.
+    absurd (InA eqke (k, e) ((k, e) :: l));auto with smtcoq_array.
   Qed.
 
   Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
   Proof.
     intros m.
-    case m;auto.
+    case m;auto with smtcoq_array.
     intros p l abs.
     inversion abs.
   Qed.
@@ -494,15 +494,15 @@ Module Raw.
     - simpl. case_eq (compare x k'); trivial.
       + intros _x0 e0.
         absurd (In x ((k', _x) :: l));try assumption.
-        apply Sort_Inf_NotIn with _x;auto.
+        apply Sort_Inf_NotIn with _x;auto with smtcoq_array.
       + intros _x0 e0.
         apply IHb.
-        elim (sort_inv sorted);auto.
-        elim (In_inv belong1);auto.
+        elim (sort_inv sorted);auto with smtcoq_array.
+        elim (In_inv belong1);auto with smtcoq_array.
         intro abs.
-        absurd (eq x k'); auto.
+        absurd (eq x k'); auto with smtcoq_array.
         symmetry in abs.
-        apply lt_not_eq in abs; auto.
+        apply lt_not_eq in abs; auto with smtcoq_array.
   Qed.
 
   Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m.
@@ -510,10 +510,10 @@ Module Raw.
     intros m Hm x; generalize Hm; clear Hm; unfold In,MapsTo.
     induction m as [ |[k' _x] l IHb]; intros sorted hyp;try ((inversion hyp);fail).
     revert hyp. simpl. case_eq (compare x k'); intros _x0 e0 hyp;try ((inversion hyp);fail).
-    - exists _x; auto.
-    - induction IHb; auto.
-      + exists x0; auto.
-      + inversion_clear sorted; auto.
+    - exists _x; auto with smtcoq_array.
+    - induction IHb; auto with smtcoq_array.
+      + exists x0; auto with smtcoq_array.
+      + inversion_clear sorted; auto with smtcoq_array.
   Qed.
 
   Lemma mem_3 : forall m (Hm:Sort m) x, mem x m = false -> ~ In x m.
@@ -539,8 +539,8 @@ Module Raw.
   Lemma find_2 :  forall m x e, find x m = Some e -> MapsTo x e m.
   Proof.
     intros m x. unfold MapsTo.
-    induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto).
-    case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto.
+    induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto with smtcoq_array).
+    case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto with smtcoq_array.
   Qed.
 
   Lemma find_1 :  forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e.
@@ -551,11 +551,11 @@ Module Raw.
     - case_eq (compare x k'); intros _x0 e1; subst.
       + inversion_clear 2.
         * clear e1;compute in H0; destruct H0.
-          apply lt_not_eq in H; auto. now contradict H.
+          apply lt_not_eq in H; auto with smtcoq_array. now contradict H.
         * clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute.
           (* order. *)
           intros.
-          apply (lt_trans k') in _x0; auto.
+          apply (lt_trans k') in _x0; auto with smtcoq_array.
           apply lt_not_eq in _x0.
           now contradict _x0.
       + clear e1;inversion_clear 2.
@@ -564,7 +564,7 @@ Module Raw.
           (* order. *)
           intros.
           apply lt_not_eq in H. now contradict H.
-      + clear e1; do 2 inversion_clear 1; auto.
+      + clear e1; do 2 inversion_clear 1; auto with smtcoq_array.
         compute in H2; destruct H2.
         (* order. *)
         subst. apply lt_not_eq in _x0. now contradict _x0.
@@ -587,7 +587,7 @@ Module Raw.
   Proof.
     intros m x y e; generalize y; clear y.
     unfold MapsTo.
-    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto.
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1]; simpl; auto with smtcoq_array.
   Qed.
 
   Lemma add_2 : forall m x y e e',
@@ -595,14 +595,14 @@ Module Raw.
   Proof.
     intros m x  y e e'.
     generalize y e; clear y e; unfold MapsTo.
-    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto;  clear e0.
-    subst;auto.
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e0];simpl;auto with smtcoq_array;  clear e0.
+    subst;auto with smtcoq_array.
 
     intros y' e'' eqky';  inversion_clear 1;  destruct H0; simpl in *.
     (* order. *)
     subst. now contradict eqky'.
-    auto.
-    auto.
+    auto with smtcoq_array.
+    auto with smtcoq_array.
     intros y' e'' eqky'; inversion_clear 1; intuition.
   Qed.
 
@@ -611,10 +611,10 @@ Module Raw.
   Proof.
     intros m x y e e'. generalize y e; clear y e; unfold MapsTo.
     induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];simpl; intros.
-    apply (In_inv_3 H0); compute; auto.
-    apply (In_inv_3 H0); compute; auto.
-    constructor 2; apply (In_inv_3 H0); compute; auto.
-    inversion_clear H0; auto.
+    apply (In_inv_3 H0); compute; auto with smtcoq_array.
+    apply (In_inv_3 H0); compute; auto with smtcoq_array.
+    constructor 2; apply (In_inv_3 H0); compute; auto with smtcoq_array.
+    inversion_clear H0; auto with smtcoq_array.
   Qed.
 
   Lemma add_Inf : forall (m:farray)(x x':key)(e e':elt),
@@ -628,7 +628,7 @@ Module Raw.
     compute in H0,H1.
     simpl; case (compare x x''); intuition.
   Qed.
-  Hint Resolve add_Inf.
+  Hint Resolve add_Inf : smtcoq_array.
 
   Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m).
   Proof.
@@ -636,9 +636,9 @@ Module Raw.
     simpl; intuition.
     intros.
     destruct a as (x',e').
-    simpl; case (compare x x'); intuition; inversion_clear Hm; auto.
-    constructor; auto.
-    apply Inf_eq with (x',e'); auto.
+    simpl; case (compare x x'); intuition; inversion_clear Hm; auto with smtcoq_array.
+    constructor; auto with smtcoq_array.
+    apply Inf_eq with (x',e'); auto with smtcoq_array.
   Qed.
 
   (** * [remove] *)
@@ -661,22 +661,22 @@ Module Raw.
 
     red; inversion 1; inversion H0.
 
-    apply Sort_Inf_NotIn with x0; auto.
+    apply Sort_Inf_NotIn with x0; auto with smtcoq_array.
 
     clear e0. inversion Hm. subst.
-    apply Sort_Inf_NotIn with x0; auto.
+    apply Sort_Inf_NotIn with x0; auto with smtcoq_array.
 
     (* clear e0;inversion_clear Hm. *)
-    (* apply Sort_Inf_NotIn with x0; auto. *)
-    (* apply Inf_eq with (k',x0);auto; compute; apply eq_trans with x; auto. *)
+    (* apply Sort_Inf_NotIn with x0; auto with smtcoq_array. *)
+    (* apply Inf_eq with (k',x0);auto with smtcoq_array; compute; apply eq_trans with x; auto with smtcoq_array. *)
 
     clear e0;inversion_clear Hm.
-    assert (notin:~ In y (remove y l)) by auto.
+    assert (notin:~ In y (remove y l)) by auto with smtcoq_array.
     intros (x1,abs).
     inversion_clear abs.
     compute in H1; destruct H1.
     subst. apply lt_not_eq in _x; now contradict _x.
-    apply notin; exists x1; auto.
+    apply notin; exists x1; auto with smtcoq_array.
   Qed.
 
 
@@ -684,41 +684,41 @@ Module Raw.
       ~ eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
   Proof.
     intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo.
-    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto;
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array;
       match goal with
       | [H: compare _ _ = _ |- _ ] => clear H
       | _ => idtac
       end.
 
-    inversion_clear 3; auto.
+    inversion_clear 3; auto with smtcoq_array.
     compute in H1; destruct H1.
     subst; now contradict H.
-    inversion_clear 1; inversion_clear 2; auto.
+    inversion_clear 1; inversion_clear 2; auto with smtcoq_array.
   Qed.
 
   Lemma remove_3 : forall m (Hm:Sort m) x y e,
       MapsTo y e (remove x m) -> MapsTo y e m.
   Proof.
     intros m Hm x y e; generalize Hm; clear Hm; unfold MapsTo.
-    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto.
-    inversion_clear 1; inversion_clear 1; auto.
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array.
+    inversion_clear 1; inversion_clear 1; auto with smtcoq_array.
   Qed.
 
   Lemma remove_4_aux : forall m (Hm:Sort m) x y,
       ~ eq x y -> In y m -> In y (remove x m).
   Proof.
     intros m Hm x y; generalize Hm; clear Hm.
-    induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto;
+    induction m as [ |[k' x0] l IHf]; simpl; [ |case_eq (compare x k'); intros _x e1];subst;auto with smtcoq_array;
       match goal with
       | [H: compare _ _ = _ |- _ ] => clear H
       | _ => idtac
       end.
     rewrite In_alt.
-    inversion_clear 3; auto.
+    inversion_clear 3; auto with smtcoq_array.
     inversion H2.
     unfold eqk in H3. simpl in H3. subst. now contradict H0.
     apply In_alt.
-    exists x. auto.
+    exists x. auto with smtcoq_array.
     apply lt_not_eq in _x.
     intros.
     inversion_clear Hm.
@@ -729,27 +729,27 @@ Module Raw.
     destruct (eq_dec k' y).
     exists x0.
     apply InA_cons_hd.
-    split; simpl; auto.
+    split; simpl; auto with smtcoq_array.
     inversion H3.
     unfold eqk in H4. simpl in H4; subst. now contradict n.
     assert ((exists e : elt, MapsTo y e (remove x l)) -> (exists e : elt, MapsTo y e ((k', x0) :: remove x l))).
     intros.
     destruct H6. exists x2.
-    apply InA_cons_tl. auto.
+    apply InA_cons_tl. auto with smtcoq_array.
     apply H6.
-    apply IHf; auto.
+    apply IHf; auto with smtcoq_array.
     apply In_alt.
-    exists x1. auto.
+    exists x1. auto with smtcoq_array.
   Qed.
 
   Lemma remove_4 : forall m (Hm:Sort m) x y,
       ~ eq x y -> In y m <-> In y (remove x m).
   Proof.
     split.
-    apply remove_4_aux; auto.
+    apply remove_4_aux; auto with smtcoq_array.
     revert H.
     generalize Hm; clear Hm.
-    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto;
+    induction m as [ |[k' _x] l IHb]; simpl; [ |case_eq (compare x k'); intros _x0 e1];subst;auto with smtcoq_array;
       match goal with
       | [H: compare _ _ = _ |- _ ] => clear H
       | _ => idtac
@@ -758,7 +758,7 @@ Module Raw.
     (* rewrite In_alt in *. *)
     destruct H0 as (e, H0).
     exists e.
-    apply InA_cons_tl. auto.
+    apply InA_cons_tl. auto with smtcoq_array.
     intros.
     apply lt_not_eq in _x0.
     inversion_clear Hm.
@@ -766,11 +766,11 @@ Module Raw.
     destruct H0.
     (* destruct (eq_dec k' y). *)
     exists _x.
-    apply InA_cons_hd. split; simpl; auto.
+    apply InA_cons_hd. split; simpl; auto with smtcoq_array.
     specialize (IHb H1 H H0).
     inversion IHb.
     exists x0.
-    apply InA_cons_tl. auto.
+    apply InA_cons_tl. auto with smtcoq_array.
   Qed.
 
   Lemma remove_Inf : forall (m:farray)(Hm : Sort m)(x x':key)(e':elt),
@@ -784,9 +784,9 @@ Module Raw.
     compute in H0.
     simpl; case (compare x x''); intuition.
     inversion_clear Hm.
-    apply Inf_lt with (x'',e''); auto.
+    apply Inf_lt with (x'',e''); auto with smtcoq_array.
   Qed.
-  Hint Resolve remove_Inf.
+  Hint Resolve remove_Inf : smtcoq_array.
 
   Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m).
   Proof.
@@ -794,7 +794,7 @@ Module Raw.
     simpl; intuition.
     intros.
     destruct a as (x',e').
-    simpl; case (compare x x'); intuition; inversion_clear Hm; auto.
+    simpl; case (compare x x'); intuition; inversion_clear Hm; auto with smtcoq_array.
   Qed.
 
   (** * [elements] *)
@@ -804,25 +804,25 @@ Module Raw.
   Lemma elements_1 : forall m x e,
       MapsTo x e m -> InA eqke (x,e) (elements m).
   Proof.
-    auto.
+    auto with smtcoq_array.
   Qed.
 
   Lemma elements_2 : forall m x e,
       InA eqke (x,e) (elements m) -> MapsTo x e m.
   Proof.
-    auto.
+    auto with smtcoq_array.
   Qed.
 
   Lemma elements_3 : forall m (Hm:Sort m), sort ltk (elements m).
   Proof.
-    auto.
+    auto with smtcoq_array.
   Qed.
 
   Lemma elements_3w : forall m (Hm:Sort m), NoDupA (elements m).
   Proof.
     intros.
     apply Sort_NoDupA.
-    apply elements_3; auto.
+    apply elements_3; auto with smtcoq_array.
   Qed.
 
   (** * [fold] *)
@@ -836,7 +836,7 @@ Module Raw.
   Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A),
       fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
   Proof.
-    intros; revert i; induction m as [ |[k e]]; simpl; auto.
+    intros; revert i; induction m as [ |[k e]]; simpl; auto with smtcoq_array.
   Qed.
 
   (** * [equal] *)
@@ -860,7 +860,7 @@ Module Raw.
       Equivb cmp m m' -> equal cmp m m' = true.
   Proof.
     intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
-    revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto; unfold Equivb; intuition; subst.
+    revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; auto with smtcoq_array; unfold Equivb; intuition; subst.
     - destruct (H0 x') as [_ H3].
       assert (H2: In x' nil).
       {
@@ -873,53 +873,53 @@ Module Raw.
         apply H3. exists e. now constructor.
       }
       elim H2. intros x0 Hx0. inversion Hx0.
-    - case_eq (compare x x'); simpl; subst;auto; unfold Equivb;
+    - case_eq (compare x x'); simpl; subst;auto with smtcoq_array; unfold Equivb;
       intuition; subst.
       + destruct (H0 x).
         assert (In x ((x',e')::l')).
-        apply H2; auto.
-        exists e; auto.
+        apply H2; auto with smtcoq_array.
+        exists e; auto with smtcoq_array.
         destruct (In_inv H4).
         (* order. *)
         clear H. apply lt_not_eq in l0; now contradict l0.
         inversion_clear Hm'.
         assert (Inf (x,e) l').
-        apply Inf_lt with (x',e'); auto.
+        apply Inf_lt with (x',e'); auto with smtcoq_array.
         elim (Sort_Inf_NotIn H6 H8 H5).
       + match goal with H: compare _ _ = _ |- _ => clear H end.
         assert (cmp_e_e':cmp e e' = true).
-        apply H1 with x'; auto.
+        apply H1 with x'; auto with smtcoq_array.
         rewrite cmp_e_e'; simpl.
-        apply IHl; auto.
-        inversion_clear Hm; auto.
-        inversion_clear Hm'; auto.
+        apply IHl; auto with smtcoq_array.
+        inversion_clear Hm; auto with smtcoq_array.
+        inversion_clear Hm'; auto with smtcoq_array.
         unfold Equivb; intuition.
         destruct (H0 k).
         assert (In k ((x',e) ::l)).
-        destruct H as (e'', hyp); exists e''; auto.
-        destruct (In_inv (H2 H4)); auto.
+        destruct H as (e'', hyp); exists e''; auto with smtcoq_array.
+        destruct (In_inv (H2 H4)); auto with smtcoq_array.
         inversion_clear Hm.
         elim (Sort_Inf_NotIn H6 H7).
-        destruct H as (e'', hyp); exists e''; auto.
-        apply MapsTo_eq with k; auto.
+        destruct H as (e'', hyp); exists e''; auto with smtcoq_array.
+        apply MapsTo_eq with k; auto with smtcoq_array.
         destruct (H0 k).
         assert (In k ((x',e') ::l')).
-        destruct H as (e'', hyp); exists e''; auto.
-        destruct (In_inv (H3 H4)); auto.
+        destruct H as (e'', hyp); exists e''; auto with smtcoq_array.
+        destruct (In_inv (H3 H4)); auto with smtcoq_array.
         subst.
         inversion_clear Hm'.
         now elim (Sort_Inf_NotIn H5 H6).
-        apply H1 with k; destruct (eq_dec x' k); auto.
+        apply H1 with k; destruct (eq_dec x' k); auto with smtcoq_array.
       + destruct (H0 x').
         assert (In x' ((x,e)::l)).
-        apply H3; auto.
-        exists e'; auto.
+        apply H3; auto with smtcoq_array.
+        exists e'; auto with smtcoq_array.
         destruct (In_inv H4).
         (* order. *)
         clear H; subst; apply lt_not_eq in l0; now contradict l0.
         inversion_clear Hm.
         assert (Inf (x',e') l).
-        apply Inf_lt with (x,e); auto.
+        apply Inf_lt with (x,e); auto with smtcoq_array.
         elim (Sort_Inf_NotIn H6 H8 H5).
   Qed.
 
@@ -927,7 +927,7 @@ Module Raw.
       equal cmp m m' = true -> Equivb cmp m m'.
   Proof.
     intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'.
-    revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto; unfold Equivb;
+    revert m'; induction m as [ |[x e] l IHl]; intros [ |[x' e'] l']; simpl; subst;auto with smtcoq_array; unfold Equivb;
       intuition; try discriminate; subst;
         try match goal with H: compare _ _ = _ |- _ => clear H end.
     - inversion H0.
@@ -936,19 +936,19 @@ Module Raw.
       destruct (andb_prop _ _ H); clear H.
       destruct (IHl _ H1 H4 H7).
       destruct (In_inv H0).
-      exists e'; constructor; split; trivial; apply eq_trans with x; auto.
+      exists e'; constructor; split; trivial; apply eq_trans with x; auto with smtcoq_array.
       destruct (H k).
       destruct (H10 H9) as (e'',hyp).
-      exists e''; auto.
+      exists e''; auto with smtcoq_array.
     - revert H; case_eq (compare x x'); intros _x _ H; try inversion H.
       inversion_clear Hm;inversion_clear Hm'.
       destruct (andb_prop _ _ H); clear H.
       destruct (IHl _ H1 H4 H7).
       destruct (In_inv H0).
-      exists e; constructor; split; trivial; apply eq_trans with x'; auto.
+      exists e; constructor; split; trivial; apply eq_trans with x'; auto with smtcoq_array.
       destruct (H k).
       destruct (H11 H9) as (e'',hyp).
-      exists e''; auto.
+      exists e''; auto with smtcoq_array.
     - revert H; case_eq (compare x x'); intros _x _ H; [inversion H| |inversion H].
       inversion_clear Hm;inversion_clear Hm'.
       destruct (andb_prop _ _ H); clear H.
@@ -956,16 +956,16 @@ Module Raw.
       inversion_clear H0.
       + destruct H9; simpl in *; subst.
         inversion_clear H1.
-        * destruct H0; simpl in *; subst; auto.
+        * destruct H0; simpl in *; subst; auto with smtcoq_array.
         * elim (Sort_Inf_NotIn H4 H5).
-          exists e'0; apply MapsTo_eq with x'; auto.
+          exists e'0; apply MapsTo_eq with x'; auto with smtcoq_array.
       (* order. *)
       + inversion_clear H1.
-        * destruct H0; simpl in *; subst; auto.
+        * destruct H0; simpl in *; subst; auto with smtcoq_array.
           elim (Sort_Inf_NotIn H2 H3).
-          exists e0; apply MapsTo_eq with x'; auto.
+          exists e0; apply MapsTo_eq with x'; auto with smtcoq_array.
         (* order. *)
-        * apply H8 with k; auto.
+        * apply H8 with k; auto with smtcoq_array.
   Qed.
 
   (** This lemma isn't part of the spec of [Equivb], but is used in [FMapAVL] *)
@@ -979,18 +979,18 @@ Module Raw.
     inversion H0; subst.
     destruct x; destruct y; compute in H1, H2.
     split; intros.
-    apply equal_2; auto.
+    apply equal_2; auto with smtcoq_array.
     simpl.
     case (compare k k0);
     subst; intro HH; try (apply lt_not_eq in HH; now contradict HH).
     rewrite H2; simpl.
-    apply equal_1; auto.
-    apply equal_2; auto.
+    apply equal_1; auto with smtcoq_array.
+    apply equal_2; auto with smtcoq_array.
     generalize (equal_1 H H0 H3).
     simpl.
     case (compare k k0);
     subst; intro HH; try (apply lt_not_eq in HH; now contradict HH).
-    rewrite H2; simpl; auto.
+    rewrite H2; simpl; auto with smtcoq_array.
   Qed.
 
 End Array.
@@ -1580,7 +1580,7 @@ Section FArray.
     intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff.
     apply add_neq_mapsto_iff; auto.
   Qed.
-  Hint Resolve add_neq_o.
+  Hint Resolve add_neq_o : smtcoq_array.
 
   Lemma MapsTo_fun : forall m x (e e':elt),
       MapsTo x e m -> MapsTo x e' m -> e=e'.
@@ -1838,6 +1838,8 @@ Arguments extensionnality2 {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
 Arguments select_at_diff {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} {_} _ _ _.
 
 
+Declare Scope farray_scope.
+
 Notation "a '[' i ']'" := (select a i) (at level 1, format "a [ i ]") : farray_scope.
 Notation "a '[' i '<-' v ']'" := (store a i v)
    (at level 1, format "a [ i  <-  v ]") : farray_scope.
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index a53970b..6d64190 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -2684,6 +2684,8 @@ Qed.
 
 End RAWBITVECTOR_LIST.
 
+Declare Scope bv_scope.
+
 Module BITVECTOR_LIST <: BITVECTOR.
 
   Include RAW2BITVECTOR(RAWBITVECTOR_LIST).
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 84df9bd..0f5bc1a 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -1554,7 +1554,7 @@ Proof. intros l a H.
 
        rewrite H.
        unfold RAWBITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.size, RAWBITVECTOR_LIST.bits in *.
-       rewrite RAWBITVECTOR_LIST.List_eq_refl; auto.
+       rewrite RAWBITVECTOR_LIST.List_eq_refl; auto with smtcoq_core.
        apply inj_iff in wf0. now do 2 rewrite id' in wf0.
 
 Qed.
diff --git a/src/euf/Euf.v b/src/euf/Euf.v
index 7818246..5b4fa93 100644
--- a/src/euf/Euf.v
+++ b/src/euf/Euf.v
@@ -180,7 +180,7 @@ Section certif.
       apply C.interp_true.
       destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial.
     Qed.
-    Hint Resolve valid_C_true.
+    Hint Resolve valid_C_true : smtcoq_euf.
 
     Local Notation interp := (Atom.interp t_i t_func t_atom).
 
@@ -210,9 +210,9 @@ Section certif.
       C.interp rho (get_eq (Lit.blit l) f).
     Proof.
       intros l f Hf;unfold get_eq.
-      case_eq (t_form.[Lit.blit l]);trivial;intros.
-      case_eq (t_atom.[i]);trivial;intros.
-      destruct b;trivial.
+      case_eq (t_form.[Lit.blit l]);trivial with smtcoq_euf;intros.
+      case_eq (t_atom.[i]);trivial with smtcoq_euf;intros.
+      destruct b;trivial with smtcoq_euf.
       generalize wt_t_atom;unfold Atom.wt;unfold is_true;
        rewrite PArray.forallbi_spec;intros.
       assert (i < length t_atom).
@@ -279,48 +279,48 @@ Section certif.
        C.interp rho (check_trans_aux t1 t2 eqs res c).
     Proof.
       induction eqs;simpl;intros.
-      apply get_eq_interp;intros.
+      - apply get_eq_interp;intros.
       match goal with |- context [if ?b then _ else _] => case_eq b end;
-       intros;trivial.
+       intros;trivial with smtcoq_euf.
       simpl;rewrite Lit.interp_lit;unfold Var.interp.
-      destruct H1;[ | rewrite H1,orb_true_r;auto].
+      destruct H1;[ | rewrite H1,orb_true_r;auto with smtcoq_euf smtcoq_core].
       rewrite orb_true_iff, !andb_true_iff in H7;destruct H7 as
         [[H7 H8] | [H7 H8]].
       rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst.
-      tunicity. subst t. rewrite H4, H1;auto.
+      tunicity. subst t. rewrite H4, H1;auto with smtcoq_euf smtcoq_core.
       rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst.
-      tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto.
-      apply get_eq_interp;intros.
+      tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto with smtcoq_euf smtcoq_core.
+      - apply get_eq_interp;intros.
       destruct (Int63Properties.reflect_eqb t2 b);subst;tunicity; try subst t.
-      apply (IHeqs u);trivial.
+      + apply (IHeqs u);trivial.
       simpl;unfold is_true;rewrite orb_true_iff.
       rewrite Lit.interp_nlit;unfold Var.interp.
-      (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *)
+      (* Warning: here, we use decidability of equality over u *)
       case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
       destruct H1;[left | auto].
       apply interp_binop_eqb_trans with (4:= H1);trivial.
       rewrite interp_binop_eqb_sym;trivial.
-      destruct (Int63Properties.reflect_eqb t2 a0); subst;tunicity; try subst t.
-      apply (IHeqs u);trivial.
+      + destruct (Int63Properties.reflect_eqb t2 a0); subst;tunicity; try subst t.
+      * apply (IHeqs u);trivial.
       simpl;unfold is_true;rewrite orb_true_iff.
       rewrite Lit.interp_nlit;unfold Var.interp.
-      (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *)
+      (* Warning: here, we use decidability of equality over u *)
       case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
       destruct H1;[left | auto].
       apply interp_binop_eqb_trans with (4:= H1);trivial.
-      destruct (Int63Properties.reflect_eqb t1 b);subst;tunicity; try subst t.
-      apply (IHeqs u);trivial.
+      * destruct (Int63Properties.reflect_eqb t1 b);subst;tunicity; try subst t.
+      -- apply (IHeqs u);trivial.
       simpl;unfold is_true;rewrite orb_true_iff.
       rewrite Lit.interp_nlit;unfold Var.interp.
-      (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *)
+      (* Warning: here, we use decidability of equality over u *)
       case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
       destruct H1;[left | auto].
       apply interp_binop_eqb_trans with (5:= H1);trivial.
-      destruct (Int63Properties.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto].
+      -- destruct (Int63Properties.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto with smtcoq_euf smtcoq_core].
       apply (IHeqs u);trivial.
       simpl;unfold is_true;rewrite orb_true_iff.
       rewrite Lit.interp_nlit;unfold Var.interp.
-      (* Attention ici on utilise la decidabilit'e de l'egalit'e sur u *)
+      (* Warning: here, we use decidability of equality over u *)
       case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto].
       destruct H1;[left | auto].
       apply interp_binop_eqb_trans with (5:= H1);trivial.
@@ -332,9 +332,9 @@ Section certif.
        C.interp rho (check_trans res eqs).
     Proof.
       unfold check_trans;intros res [ | leq eqs].
-      apply get_eq_interp;intros.
+      - apply get_eq_interp;intros.
       destruct (Int63Properties.reflect_eqb a b).
-      unfold C.interp; simpl; rewrite orb_false_r.
+      + unfold C.interp; simpl; rewrite orb_false_r.
       unfold Lit.interp; simpl; rewrite Lit.is_pos_lit.
       unfold Var.interp; simpl; rewrite Lit.blit_lit.
       rewrite H1.
@@ -344,12 +344,12 @@ Section certif.
       unfold Atom.interp_hatom.
       rewrite HHb;simpl;rewrite Typ.cast_refl;simpl.
       apply Typ.i_eqb_refl.
-      auto.
-      apply get_eq_interp;intros.
+      + auto with smtcoq_euf.
+      - apply get_eq_interp;intros.
       apply check_trans_aux_correct with t;trivial.
       simpl;rewrite Lit.interp_nlit;unfold Var.interp. rewrite <- H1.
       (* Attention ici on utilise la decidabilit'e de l'egalit'e sur t *)
-      destruct (rho (Lit.blit leq));auto.
+      destruct (rho (Lit.blit leq));auto with smtcoq_core.
     Qed.
 
     Inductive Forall2 A B (P:A->B->Prop) : list A -> list B -> Prop :=
@@ -362,16 +362,16 @@ Section certif.
       (Forall2 _ _ (fun a b => interp_hatom a = interp_hatom b) l r -> C.interp rho c) ->
       C.interp rho (build_congr lp l r c).
     Proof.
-      induction lp;destruct l;destruct r;simpl;trivial;intros.
+      induction lp;destruct l;destruct r;simpl;trivial with smtcoq_euf smtcoq_core;intros.
       apply H;constructor.
       destruct a.
       apply get_eq_interp;intros.
       match goal with |- context [if ?x then _ else _] =>
-       case_eq x;intros;auto end.
+       case_eq x;intros;auto with smtcoq_euf smtcoq_core end.
       apply IHlp;simpl;intros.
       rewrite Lit.interp_nlit;unfold Var.interp.
-      case_eq (rho (Lit.blit i1));intros;simpl;[ | auto].
-      apply H;constructor;trivial.
+      case_eq (rho (Lit.blit i1));intros;simpl;[ | auto with smtcoq_euf smtcoq_core].
+      apply H;constructor;trivial with smtcoq_euf smtcoq_core.
       generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H3. rewrite Typ.eqb_spec in H4. unfold Atom.get_type in H3, H4. rewrite H3,H4. intros [va HHa] [vb HHb].
       revert H7;rewrite H2;unfold Atom.apply_binop; simpl.
       unfold Atom.interp_hatom.
@@ -381,11 +381,11 @@ Section certif.
       rewrite orb_true_iff, !andb_true_iff in H5;destruct H5 as
         [ [H5 H7] | [H5 H7]].
       rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst.
-      rewrite HHa, HHb;trivial.
+      rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core.
       rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst.
-      rewrite HHa, HHb;trivial.
-      destruct (Int63Properties.reflect_eqb i i0);[subst | auto].
-      apply IHlp;intros;apply H;constructor;auto.
+      rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core.
+      destruct (Int63Properties.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core].
+      apply IHlp;intros;apply H;constructor;auto with smtcoq_euf smtcoq_core.
     Qed.
 
     Lemma valid_check_congr :
@@ -393,71 +393,71 @@ Section certif.
           C.interp rho (check_congr leq eqs).
     Proof.
       unfold check_congr;intros leq eqs;apply get_eq_interp;intros.
-      case_eq (t_atom .[ a]);intros;auto;
-      case_eq (t_atom .[ b]);intros;auto.
+      case_eq (t_atom .[ a]);intros;auto with smtcoq_euf smtcoq_core;
+      case_eq (t_atom .[ b]);intros;auto with smtcoq_euf smtcoq_core.
       (* uop *)
-      destruct (Atom.reflect_uop_eqb u u0);[subst | auto].
+      destruct (Atom.reflect_uop_eqb u u0);[subst | auto with smtcoq_euf smtcoq_core].
       apply build_congr_correct;intros.
       simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp.
       rewrite H1.
       generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb].
       unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl.
       rewrite HHb, HHa. simpl.
-      rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa.
-      rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb.
+      rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa.
+      rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb.
       rewrite Typ.cast_refl;simpl.
       assert (Atom.Bval t_i t va = Atom.Bval t_i t vb).
        inversion H6;subst.
        unfold Atom.interp_hatom in H10.
-       rewrite <- HHa; rewrite <- HHb, H10;trivial.
+       rewrite <- HHa; rewrite <- HHb, H10;trivial with smtcoq_euf smtcoq_core.
        inversion H7.
-       apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial.
+       apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core.
        rewrite H9.
        apply Typ.i_eqb_refl.
-      intros x y;destruct (Typ.reflect_eqb x y);auto.
+      intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core.
       (* bop *)
-      destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto].
+      destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto with smtcoq_euf smtcoq_core].
       apply build_congr_correct;intros.
       simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp.
       rewrite H1.
       generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb].
       unfold Atom.apply_binop. unfold Atom.interp_hatom;simpl.
       rewrite HHb, HHa;simpl.
-      rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa.
-      rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb.
+      rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa.
+      rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb.
       rewrite Typ.cast_refl;simpl.
       assert (Atom.Bval t_i t va = Atom.Bval t_i t vb).
        inversion H6;clear H6;subst.
        inversion H12;clear H12;subst.
        unfold Atom.interp_hatom in H10, H8.
-       rewrite <- HHa. rewrite <- HHb, H10, H8;trivial.
+       rewrite <- HHa. rewrite <- HHb, H10, H8;trivial with smtcoq_euf smtcoq_core.
       inversion H7.
-      apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial.
+      apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core.
       rewrite H9.
       apply Typ.i_eqb_refl.
-      intros x y;destruct (Typ.reflect_eqb x y);auto.
+      intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core.
       (* op *)
-      destruct (Int63Properties.reflect_eqb i i0);[subst | auto].
+      destruct (Int63Properties.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core].
       apply build_congr_correct;intros.
       simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp.
       rewrite H1.
       generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb].
       unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl.
       rewrite HHb, HHa;simpl.
-      rewrite Atom.t_interp_wf in HHa; auto. rewrite H4 in HHa. simpl in HHa.
-      rewrite Atom.t_interp_wf in HHb; auto. rewrite H5 in HHb. simpl in HHb.
+      rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa.
+      rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb.
       rewrite Typ.cast_refl;simpl.
       assert (Atom.Bval t_i t va = Atom.Bval t_i t vb).
         rewrite <- HHa;rewrite <- HHb;destruct (t_func.[i0]).
         apply f_equal;clear HHa HHb va vb H5 H4.
-        induction H6;simpl;trivial.
+        induction H6;simpl;trivial with smtcoq_euf smtcoq_core.
         unfold Atom.interp_hatom in H4.
-        rewrite IHForall2, H4;trivial.
+        rewrite IHForall2, H4;trivial with smtcoq_euf smtcoq_core.
       inversion H7.
-      apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial.
+      apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core.
       rewrite H9.
       apply Typ.i_eqb_refl.
-      intros x y;destruct (Typ.reflect_eqb x y);auto.
+      intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core.
     Qed.
 
     Lemma valid_check_congr_pred :
@@ -465,11 +465,11 @@ Section certif.
           C.interp rho (check_congr_pred lpa lpb eqs).
     Proof.
       unfold check_congr_pred;intros.
-      case_eq (t_form.[Lit.blit lpa]);auto.
-      case_eq (t_form.[Lit.blit lpb]);auto;intros.
-      case_eq (t_atom.[i0]);auto; case_eq (t_atom.[i]);auto;intros.
+      case_eq (t_form.[Lit.blit lpa]);auto with smtcoq_euf smtcoq_core.
+      case_eq (t_form.[Lit.blit lpb]);auto with smtcoq_euf smtcoq_core;intros.
+      case_eq (t_atom.[i0]);auto with smtcoq_euf smtcoq_core; case_eq (t_atom.[i]);auto with smtcoq_euf smtcoq_core;intros.
       (* uop *)
-      destruct (Atom.reflect_uop_eqb u0 u);[subst | auto].
+      destruct (Atom.reflect_uop_eqb u0 u);[subst | auto with smtcoq_euf smtcoq_core].
       apply build_congr_correct;simpl;intros.
       rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp.
       replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)).
@@ -485,12 +485,12 @@ Section certif.
         rewrite H2, def_t_atom;discriminate.
       apply H4 in H5;apply H4 in H6;clear H4.
       unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl.
-      rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial.
+      rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core.
       apply f_equal;apply f_equal.
-      inversion H3;clear H3;subst;trivial.
+      inversion H3;clear H3;subst;trivial with smtcoq_euf smtcoq_core.
 
       (* bop *)
-      destruct (Atom.reflect_bop_eqb b0 b);[subst | auto].
+      destruct (Atom.reflect_bop_eqb b0 b);[subst | auto with smtcoq_euf smtcoq_core].
       apply build_congr_correct;simpl;intros.
       rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp.
       replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)).
@@ -506,13 +506,13 @@ Section certif.
         rewrite H2, def_t_atom;discriminate.
       apply H4 in H5;apply H4 in H6;clear H4.
       unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl.
-      rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial.
+      rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core.
       inversion H3;clear H3;subst.
       inversion H11;clear H11;subst.
-      apply f_equal; apply f_equal2;trivial.
+      apply f_equal; apply f_equal2;trivial with smtcoq_euf smtcoq_core.
 
       (* op *)
-      destruct (Int63Properties.reflect_eqb i2 i1);[subst | auto].
+      destruct (Int63Properties.reflect_eqb i2 i1);[subst | auto with smtcoq_euf smtcoq_core].
       apply build_congr_correct;simpl;intros.
       rewrite orb_false_r, Lit.interp_lit, Lit.interp_nlit;unfold Var.interp.
       replace (rho (Lit.blit lpb)) with (rho (Lit.blit lpa)).
@@ -528,11 +528,11 @@ Section certif.
         rewrite H2, def_t_atom;discriminate.
       apply H4 in H5;apply H4 in H6;clear H4.
       unfold Atom.interp_form_hatom, Atom.interp_hatom;simpl.
-      rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial.
+      rewrite !Atom.t_interp_wf, H1, H2;simpl;trivial with smtcoq_euf smtcoq_core.
       apply f_equal;destruct (t_func.[i1]);apply f_equal.
       clear H H0 H1 H2 H5 H6.
-      induction H3;simpl;trivial.
-      unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial.
+      induction H3;simpl;trivial with smtcoq_euf smtcoq_core.
+      unfold Atom.interp_hatom in H;rewrite H, IHForall2;trivial with smtcoq_euf smtcoq_core.
     Qed.
 
   End Proof.
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index c214c3b..46bbc5d 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -113,7 +113,7 @@ Section certif.
         | Some z => (vm, PEc z)
         | None =>
           let (vm,p) := find_var vm h in
-          (vm,PEX Z p)
+          (vm,PEX p)
         end
       end.
 
@@ -157,7 +157,7 @@ Section certif.
   Section Build_form.
 
     Definition build_not2 i f :=
-      fold (fun f' => N (N (A:=Formula Z) f')) 1 i f.
+      fold (fun f' : BFormula (Formula Z) => N (N f')) 1 i f.
 
     Variable build_var : vmap -> var -> option (vmap*BFormula (Formula Z)).
 
@@ -166,11 +166,11 @@ Section certif.
       match f with
         | Form.Fatom h =>
           match build_formula vm h with
-            | Some (vm,f) => Some (vm, A f)
+            | Some (vm,f) => Some (vm, A f tt)
             | None => None
           end
-        | Form.Ftrue => Some (vm, TT (Formula Z))
-        | Form.Ffalse => Some (vm, FF (Formula Z))
+        | Form.Ftrue => Some (vm, TT)
+        | Form.Ffalse => Some (vm, FF)
         | Form.Fnot2 i l =>
           match build_var vm (Lit.blit l) with
             | Some (vm, f) =>
@@ -181,7 +181,7 @@ Section certif.
           end
         | Form.Fand args =>
           let n := length args in
-          if n == 0 then Some (vm,TT (Formula Z))
+          if n == 0 then Some (vm,TT)
           else
             foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,Cj f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in
               match build_var vm (Lit.blit l) with
@@ -190,7 +190,7 @@ Section certif.
               end)
         | Form.For args =>
           let n := length args in
-          if n == 0 then Some (vm,FF (Formula Z))
+          if n == 0 then Some (vm,FF)
           else
             foldi (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,D f1' f2') | None => None end | None => None end) 1 (n-1) (let l := args.[0] in
               match build_var vm (Lit.blit l) with
@@ -211,7 +211,7 @@ Section certif.
           end
         | Form.Fimp args =>
           let n := length args in
-          if n == 0 then Some (vm,TT (Formula Z))
+          if n == 0 then Some (vm,TT)
           else if n <= 1 then
             let l := args.[0] in
             match build_var vm (Lit.blit l) with
@@ -219,7 +219,7 @@ Section certif.
               | None => None
             end
           else
-            foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,I f2' f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in
+            foldi_down (fun i f1 => match f1 with | Some(vm',f1') => let l := (args.[i]) in match build_var vm' (Lit.blit l) with | Some(vm2,f2) => let f2' := if Lit.is_pos l then f2 else N f2 in Some(vm2,I f2' None f1') | None => None end | None => None end) (n-2) 0 (let l := args.[n-1] in
               match build_var vm (Lit.blit l) with
                 | Some (vm',f) => if Lit.is_pos l then Some (vm',f) else Some (vm',N f)
                 | None => None
@@ -295,7 +295,7 @@ Section certif.
 
   Definition build_clause vm cl :=
     match build_clause_aux vm cl with
-    | Some (vm, bf) => Some (vm, I bf (FF _))
+    | Some (vm, bf) => Some (vm, I bf None FF)
     | None => None
     end.
 
@@ -479,11 +479,11 @@ Section certif.
 
     Fixpoint bounded_bformula (p:positive) (bf:BFormula (Formula Z)) :=
       match bf with
-      | @TT _ | @FF _ | @X _ _ => true
-      | A f => bounded_formula p f
+      | @TT _ | @FF _ | @X _ _ _ _ _ => true
+      | A f _ => bounded_formula p f
       | Cj bf1 bf2
       | D bf1 bf2
-      | I bf1 bf2 => bounded_bformula p bf1 && bounded_bformula p bf2
+      | I bf1 _ bf2 => bounded_bformula p bf1 && bounded_bformula p bf2
       | N bf => bounded_bformula p bf
       end.
 
@@ -523,7 +523,7 @@ Section certif.
        check_atom h Typ.TZ ->
        match build_z_atom h with
        | Some z => (vm, PEc z)
-       | None => let (vm0, p) := find_var vm h in (vm0, PEX Z p)
+       | None => let (vm0, p) := find_var vm h in (vm0, PEX p)
        end = (vm', pe) ->
        wf_vmap vm ->
        wf_vmap vm' /\
@@ -1020,13 +1020,15 @@ 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 forallbi_spec in wt_t_atom.
-      case_eq (h < length t_atom);intros Heq;unfold get_type;auto.
+      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.
     Qed.
 
 
+    Local Notation eval_f := (eval_f (fun x => x)).
+
     Lemma build_not2_pos_correct : forall vm f l i,
       bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (build_not2 i f)).
     Proof.
@@ -1083,7 +1085,7 @@ Transparent build_z_atom.
     Proof.
       intros vm vm' Hnth.
       unfold is_true;induction bf;simpl;try tauto.
-      destruct a;unfold bounded_formula;simpl.
+      destruct t;unfold bounded_formula;simpl.
       rewrite andb_true_iff;intros (H1, H2).
       rewrite !(interp_pexpr_le _ _ Hnth);tauto.
       rewrite andb_true_iff;intros (H1,H2);rewrite IHbf1, IHbf2;tauto.
@@ -1123,12 +1125,12 @@ Transparent build_z_atom.
       (* Ftrue *)
       intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 4 split; auto.
       (* Ffalse *)
-      intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 3 (split; auto); discriminate.
+      intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate.
       (* 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; case (length l == 0).
-      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto).
+      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core).
       revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))).
       intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split.
       intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate.
@@ -1136,104 +1138,76 @@ Transparent build_z_atom.
       intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split.
       intros p H15; rewrite H7; auto; apply H12; eauto with arith.
       split.
-      simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto.
-      simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; 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); try discriminate; intros [H20 H21]; auto.
+      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; 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; case (length l == 0).
-      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto); discriminate.
+      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate.
       revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))).
-      intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split.
+      intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split.
       intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate.
-      intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto; intro H4; elim H3; rewrite <- H14; auto.
-      intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split.
-      intros p H15; rewrite H7; auto; apply H12; eauto with arith.
+      intro H3; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core.
+      intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split.
+      intros p H15; rewrite H7; auto with smtcoq_core; apply H12; eauto with smtcoq_core arith.
       split.
-      simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto.
-      simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; 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; try (intros [H20|H20]; auto; discriminate); right; intro H20; discriminate.
+      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; 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; case (length l == 0).
-      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto; split; [omega| ]; do 3 (split; auto).
+      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core).
       case (length l <= 1).
-      case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H3 [H4 [H5 [H6 H7]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split.
+      case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H3 [H4 [H5 [H6 H7]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split.
       intros H8 H9; rewrite <- H7 in H9; rewrite H9 in H8; discriminate.
-      intro H8; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto; intro H9; rewrite H7 in H9; elim H8; auto.
+      intro H8; case_eq (Var.interp rho (Lit.blit (l .[ 0]))); auto with smtcoq_core; intro H9; rewrite H7 in H9; elim H8; auto with smtcoq_core.
       revert vm' bf; apply (foldi_down_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))).
-      intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ length l - 1]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ length l - 1])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split.
+      intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ length l - 1]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ length l - 1])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split.
       intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate.
-      intro H3; case_eq (Var.interp rho (Lit.blit (l .[ length l - 1]))); auto; intro H4; elim H3; rewrite <- H14; auto.
-      intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto; split; [eauto with arith| ]; split.
-      intros p H15; rewrite H7; auto; apply H12; eauto with arith.
+      intro H3; case_eq (Var.interp rho (Lit.blit (l .[ length l - 1]))); auto with smtcoq_core; intro H4; elim H3; rewrite <- H14; auto with smtcoq_core.
+      intros i a b _ H1; case a; try discriminate; intros [vm0 f0] IH vm' bf; case_eq (build_var vm0 (Lit.blit (l .[ i]))); try discriminate; intros [vm1 f1] Heq H2 H3; inversion H2; subst vm'; subst bf; destruct (IH _ _ (refl_equal (Some (vm0, f0))) H3) as [H5 [H6 [H7 [H8 H9]]]]; destruct (Hbv _ _ _ _ Heq H5) as [H10 [H11 [H12 [H13 H14]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split.
+      intros p H15; rewrite H7; auto with smtcoq_core; apply H12; eauto with smtcoq_core arith.
       split.
-      simpl; rewrite (bounded_bformula_le _ _ H11 _ H8); case (Lit.is_pos (l .[ i])); rewrite H13; auto.
-      simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; 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]))); auto; try discriminate; simpl; intro H; apply H; discriminate.
+      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; 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]))); auto with smtcoq_core; try discriminate; simpl; intro H; apply H; discriminate.
       (* Fxor *)
-      simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto; split; [eauto with arith| ]; split.
-      intros p H18; rewrite H5; auto; rewrite H10; eauto with arith.
+      simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split.
+      intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith.
       split.
-      case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto.
-      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto; try discriminate; simpl.
-      intros [_ [H20|H20]]; elim H20; reflexivity.
-      intros _; split; [left; reflexivity|right; intro H20; discriminate].
-      intros _; split; [right; reflexivity|left; intro H20; discriminate].
-      intros [[H20|H20] _]; discriminate.
-      intros [_ [H20|H20]]; elim H20; [reflexivity|discriminate].
-      intros [[H20|H20] _]; [discriminate|elim H20; reflexivity].
-      intros _; split; [right|left]; discriminate.
-      intros [[H20|H20] _]; [elim H20; reflexivity|discriminate].
-      intros [_ [H20|H20]]; elim H20; [discriminate|reflexivity].
-      intros _; split; [left|right]; discriminate.
-      intros [[H20|H20] _]; elim H20; reflexivity.
-      intros _; split; [right; discriminate|left; intro H21; apply H21; reflexivity].
-      intros _; split; [left; discriminate|right; intro H21; apply H21; reflexivity].
-      intros [_ [H20|H20]]; elim H20; discriminate.
+      case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto with smtcoq_core.
+      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition.
       (* Fiff *)
-      simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto; split; [eauto with arith| ]; split.
-      intros p H18; rewrite H5; auto; rewrite H10; eauto with arith.
+      simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split.
+      intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith.
       split.
-      case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto.
-      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto; try discriminate; simpl.
-      intros [_ [H20|H20]]; [elim H20; reflexivity|discriminate].
-      intros [[H20|H20] _]; [discriminate|elim H20; reflexivity].
-      intros _; split; [right|left]; discriminate.
-      intros [_ [H20|H20]]; elim H20; reflexivity.
-      intros _; split; [left; reflexivity|right; discriminate].
-      intros _; split; [right; intro H20; apply H20; reflexivity|left; discriminate].
-      intros [[H20|H20] _]; [ |elim H20]; discriminate.
-      intros [[H20|H20] _]; elim H20; reflexivity.
-      intros _; split; [right; discriminate|left; intro H20; apply H20; reflexivity].
-      intros _; split; [left; discriminate|right; reflexivity].
-      intros [_ [H20|H20]]; [elim H20| ]; discriminate.
-      intros [[H20|H20] _]; elim H20; [reflexivity|discriminate].
-      intros [_ [H20|H20]]; elim H20; [discriminate|reflexivity].
-      intros _; split; [left|right]; discriminate.
+      case (Lit.is_pos a); case (Lit.is_pos b); simpl; rewrite H11; rewrite (bounded_bformula_le _ _ H9 _ H6); auto with smtcoq_core.
+      simpl; rewrite (interp_bformula_le _ _ H10 _ H6) in H7; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; unfold Lit.interp; rewrite Ha, Hb; simpl; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); case (Var.interp rho (Lit.blit b))); split; auto with smtcoq_core; try discriminate; simpl; intuition.
       (* Fite *)
-      simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2; case_eq (build_var vm2 (Lit.blit c)); try discriminate; intros [vm3 f3] Heq3 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; destruct (Hbv _ _ _ _ Heq3 H8) as [H13 [H14 [H15 [H16 H17]]]]; split; auto; split; [eauto with arith| ]; split.
-      intros p H18; rewrite H5; auto; rewrite H10; eauto with arith.
-      assert (H18: (Pos.to_nat (fst vm1) <= Pos.to_nat (fst vm3))%nat) by eauto with arith.
+      simpl; case_eq (build_var vm (Lit.blit a)); try discriminate; intros [vm1 f1] Heq1; case_eq (build_var vm1 (Lit.blit b)); try discriminate; intros [vm2 f2] Heq2; case_eq (build_var vm2 (Lit.blit c)); try discriminate; intros [vm3 f3] Heq3 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq1 H2) as [H3 [H4 [H5 [H6 H7]]]]; destruct (Hbv _ _ _ _ Heq2 H3) as [H8 [H9 [H10 [H11 H12]]]]; destruct (Hbv _ _ _ _ Heq3 H8) as [H13 [H14 [H15 [H16 H17]]]]; split; auto with smtcoq_core; split; [eauto with smtcoq_core arith| ]; split.
+      intros p H18; rewrite H5; auto with smtcoq_core; rewrite H10; eauto with smtcoq_core arith.
+      assert (H18: (Pos.to_nat (fst vm1) <= Pos.to_nat (fst vm3))%nat) by eauto with smtcoq_core arith.
       split.
-      case (Lit.is_pos a); case (Lit.is_pos b); case (Lit.is_pos c); simpl; rewrite H16; rewrite (bounded_bformula_le _ _ H14 _ H11); rewrite (bounded_bformula_le _ _ H18 _ H6); auto.
-      simpl; rewrite (interp_bformula_le _ _ H15 _ H11) in H12; rewrite (interp_bformula_le _ vm3) in H7; [ |intros p Hp; rewrite H10; eauto with arith|auto]; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; case_eq (Lit.is_pos c); intro Hc; unfold Lit.interp; rewrite Ha, Hb, Hc; simpl; rewrite <- H17; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); [case (Var.interp rho (Lit.blit b))|case (Var.interp rho (Lit.blit c))]); split; auto; try discriminate; try (intros [[H20 H21]|[H20 H21]]; auto); try (intros _; left; split; auto; discriminate); try (intros _; right; split; auto; discriminate); try (elim H20; discriminate); try (elim H21; discriminate); try (simpl; intro H; left; split; auto; discriminate); try (revert H; case (Var.interp rho (Lit.blit c)); discriminate); try (revert H; case (Var.interp rho (Lit.blit b)); discriminate); try (intro H20; rewrite H20 in H; discriminate); simpl.
-      intro H; right; split; auto.
-      intro H; right; split; auto.
-      intro H; right; split; auto.
+      case (Lit.is_pos a); case (Lit.is_pos b); case (Lit.is_pos c); simpl; rewrite H16; rewrite (bounded_bformula_le _ _ H14 _ H11); rewrite (bounded_bformula_le _ _ H18 _ H6); auto with smtcoq_core.
+      simpl; rewrite (interp_bformula_le _ _ H15 _ H11) in H12; rewrite (interp_bformula_le _ vm3) in H7; [ |intros p Hp; rewrite H10; eauto with smtcoq_core arith|auto with smtcoq_core]; case_eq (Lit.is_pos a); intro Ha; case_eq (Lit.is_pos b); intro Hb; case_eq (Lit.is_pos c); intro Hc; unfold Lit.interp; rewrite Ha, Hb, Hc; simpl; rewrite <- H17; rewrite <- H12; rewrite <- H7; (case (Var.interp rho (Lit.blit a)); [case (Var.interp rho (Lit.blit b))|case (Var.interp rho (Lit.blit c))]); split; auto with smtcoq_core; try discriminate; try (intros [[H20 H21]|[H20 H21]]; auto with smtcoq_core); try (intros _; left; split; auto with smtcoq_core; discriminate); try (intros _; right; split; auto with smtcoq_core; discriminate); try (elim H20; discriminate); try (elim H21; discriminate); try (simpl; intro H; left; split; auto with smtcoq_core; discriminate); try (revert H; case (Var.interp rho (Lit.blit c)); discriminate); try (revert H; case (Var.interp rho (Lit.blit b)); discriminate); try (intro H20; rewrite H20 in H; discriminate); simpl.
+      intro H; right; split; auto with smtcoq_core.
+      intro H; right; split; auto with smtcoq_core.
+      intro H; right; split; auto with smtcoq_core.
       intro H20; rewrite H20 in H; discriminate.
-      revert H21; case (Var.interp rho (Lit.blit c)); auto.
-      right; split; auto; intro H20; rewrite H20 in H; discriminate.
-      revert H21; case (Var.interp rho (Lit.blit c)); auto.
-      intro H; right; split; auto.
-      intro H; right; split; auto.
+      revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core.
+      right; split; auto with smtcoq_core; intro H20; rewrite H20 in H; discriminate.
+      revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core.
+      intro H; right; split; auto with smtcoq_core.
+      intro H; right; split; auto with smtcoq_core.
       intro H; left; split; try discriminate; revert H; case (Var.interp rho (Lit.blit b)); discriminate.
-      revert H21; case (Var.interp rho (Lit.blit b)); auto.
+      revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core.
       intro H; left; split; try discriminate; revert H; case (Var.interp rho (Lit.blit b)); discriminate.
-      revert H21; case (Var.interp rho (Lit.blit b)); auto.
-      intro H; right; split; auto; revert H; case (Var.interp rho (Lit.blit c)); discriminate.
-      revert H21; case (Var.interp rho (Lit.blit c)); auto.
-      intro H; right; split; auto; revert H; case (Var.interp rho (Lit.blit c)); discriminate.
-      revert H21; case (Var.interp rho (Lit.blit c)); auto.
-      intro H; left; split; auto; revert H; case (Var.interp rho (Lit.blit b)); discriminate.
-      revert H21; case (Var.interp rho (Lit.blit b)); auto.
-      intro H; left; split; auto; revert H; case (Var.interp rho (Lit.blit b)); discriminate.
-      revert H21; case (Var.interp rho (Lit.blit b)); auto.
+      revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core.
+      intro H; right; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit c)); discriminate.
+      revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core.
+      intro H; right; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit c)); discriminate.
+      revert H21; case (Var.interp rho (Lit.blit c)); auto with smtcoq_core.
+      intro H; left; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit b)); discriminate.
+      revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core.
+      intro H; left; split; auto with smtcoq_core; revert H; case (Var.interp rho (Lit.blit b)); discriminate.
+      revert H21; case (Var.interp rho (Lit.blit b)); auto with smtcoq_core.
     Qed.
 
 
@@ -1251,8 +1225,8 @@ Transparent build_z_atom.
     Proof.
       unfold build_var; apply foldi_down_cont_ind; try discriminate.
       intros i cont _ Hlen Hrec v vm vm' bf; unfold is_true; intros H1 H2; replace (Var.interp rho v) with (Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[v])).
-      apply (build_hform_correct cont); auto.
-      unfold Var.interp; rewrite <- wf_interp_form; auto.
+      apply (build_hform_correct cont); auto with smtcoq_core.
+      unfold Var.interp; rewrite <- wf_interp_form; auto with smtcoq_core.
     Qed.
 
 
@@ -1285,17 +1259,17 @@ Transparent build_z_atom.
       unfold build_nlit; intros l vm vm' bf; case_eq (build_form vm (t_form .[ Lit.blit (Lit.neg l)])); try discriminate.
       intros [vm1 f] Heq H1 H2; inversion H1; subst vm1; subst bf; case_eq (Lit.is_pos (Lit.neg l)); intro Heq2.
       replace (negb (Lit.interp rho l)) with (Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form .[ Lit.blit (Lit.neg l)])).
-      apply build_form_correct; auto.
+      apply build_form_correct; auto with smtcoq_core.
       unfold Lit.interp; replace (Lit.is_pos l) with false.
-      rewrite negb_involutive; unfold Var.interp; rewrite <- wf_interp_form; auto; rewrite Lit.blit_neg; auto.
-      rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate.
-      simpl; destruct (build_form_correct (t_form .[ Lit.blit (Lit.neg l)]) vm vm' f Heq H2) as [H3 [H4 [H5 [H6 [H7 H8]]]]]; do 4 (split; auto); split.
+      rewrite negb_involutive; unfold Var.interp; rewrite <- wf_interp_form; auto with smtcoq_core; rewrite Lit.blit_neg; auto with smtcoq_core.
+      rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto with smtcoq_core; intro H; rewrite H in Heq2; discriminate.
+      simpl; destruct (build_form_correct (t_form .[ Lit.blit (Lit.neg l)]) vm vm' f Heq H2) as [H3 [H4 [H5 [H6 [H7 H8]]]]]; do 4 (split; auto with smtcoq_core); split.
       intros H9 H10; pose (H11 := H8 H10); unfold Lit.interp in H9; replace (Lit.is_pos l) with true in H9.
-      unfold Var.interp in H9; rewrite <- wf_interp_form in H11; auto; rewrite Lit.blit_neg in H11; rewrite H11 in H9; discriminate.
-       rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate.
-       intro H9; case_eq (Lit.interp rho l); intro Heq3; auto; elim H9; apply H7; unfold Lit.interp in Heq3; replace (Lit.is_pos l) with true in Heq3.
-       unfold Var.interp in Heq3; rewrite <- wf_interp_form; auto; rewrite Lit.blit_neg; auto.
-       rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto; intro H; rewrite H in Heq2; discriminate.
+      unfold Var.interp in H9; rewrite <- wf_interp_form in H11; auto with smtcoq_core; rewrite Lit.blit_neg in H11; rewrite H11 in H9; discriminate.
+       rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto with smtcoq_core; intro H; rewrite H in Heq2; discriminate.
+       intro H9; case_eq (Lit.interp rho l); intro Heq3; auto with smtcoq_core; elim H9; apply H7; unfold Lit.interp in Heq3; replace (Lit.is_pos l) with true in Heq3.
+       unfold Var.interp in Heq3; rewrite <- wf_interp_form; auto with smtcoq_core; rewrite Lit.blit_neg; auto with smtcoq_core.
+       rewrite Lit.is_pos_neg in Heq2; case_eq (Lit.is_pos l); auto with smtcoq_core; intro H; rewrite H in Heq2; discriminate.
     Qed.
 
 
@@ -1403,7 +1377,7 @@ Transparent build_z_atom.
      rewrite H0, def_t_atom;discriminate.
      apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2.
      rewrite !andb_true_iff in H2;decompose [and] H2;clear H2.
-     apply Hf with (2:= H0);trivial. auto.
+     apply Hf with (2:= H0);trivial. auto with smtcoq_core.
      rewrite wf_interp_form, H;simpl.
      unfold Atom.interp_form_hatom, Atom.interp_hatom at 1;simpl.
      rewrite Atom.t_interp_wf, H0;simpl;trivial.
@@ -1434,7 +1408,7 @@ Transparent build_z_atom.
      rewrite H0, def_t_atom;discriminate.
      apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2.
      rewrite !andb_true_iff in H2;decompose [and] H2;clear H2.
-     simpl; apply Hf with (2:= H0);trivial. auto.
+     simpl; apply Hf with (2:= H0);trivial. auto with smtcoq_core.
      rewrite wf_interp_form, H;simpl.
      unfold Atom.interp_form_hatom, Atom.interp_hatom at 1;simpl.
      rewrite Atom.t_interp_wf, H0;simpl;trivial.
@@ -1480,7 +1454,7 @@ Transparent build_z_atom.
      case_eq (build_clause empty_vmap cl).
      intros (vm1, bf) Heq.
      destruct (build_clause_correct _ _ _ _ Heq).
-      red;simpl;auto.
+      red;simpl;auto with smtcoq_core.
      decompose [and] H0.
      case_eq (ZTautoChecker bf c);intros Heq2.
      unfold C.valid;rewrite H5.
@@ -1512,11 +1486,11 @@ Transparent build_z_atom.
      rewrite wf_interp_form, H;simpl.
      case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])).
      intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19.
-     apply (afold_left_orb_true int 0); subst; auto.
+     apply (afold_left_orb_true int 0); subst; auto with smtcoq_core.
      apply ltb_spec;rewrite H0;compute;trivial.
-     apply (afold_left_orb_true int 1); auto.
+     apply (afold_left_orb_true int 1); auto with smtcoq_core.
      apply ltb_spec;rewrite H0;compute;trivial.
-     apply (afold_left_orb_true int 2); auto.
+     apply (afold_left_orb_true int 2); auto with smtcoq_core.
      apply ltb_spec;rewrite H0;compute;trivial.
      intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19.
      unfold Lit.interp in H19.
@@ -1534,7 +1508,7 @@ Transparent build_z_atom.
      destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) Typ.TZ) as [H12|H12]; [intros _|discriminate].
      generalize H6. clear H6.
      destruct (Typ.reflect_eqb (get_type t_i t_func t_atom b0) t) as [H6|H6]; [intros _|discriminate].
-     rewrite <- H6. auto.
+     rewrite <- H6. auto with smtcoq_core.
      rewrite H26 in H19.
      case_eq (interp_atom (t_atom .[ b1])); intros t1 v1 Heq1.
      assert (H50: t1 = Typ.TZ).
@@ -1560,11 +1534,11 @@ Transparent build_z_atom.
      rewrite wf_interp_form, H;simpl.
      case_eq (Lit.interp rho (a.[0]) || Lit.interp rho (a.[1]) || Lit.interp rho (a.[2])).
      intros;repeat (rewrite orb_true_iff in H19);destruct H19. destruct H19.
-     apply (afold_left_orb_true int 0); auto.
+     apply (afold_left_orb_true int 0); auto with smtcoq_core.
      apply ltb_spec;rewrite H0;compute;trivial.
-     apply (afold_left_orb_true int 1); auto.
+     apply (afold_left_orb_true int 1); auto with smtcoq_core.
      apply ltb_spec;rewrite H0;compute;trivial.
-     apply (afold_left_orb_true int 2); auto.
+     apply (afold_left_orb_true int 2); auto with smtcoq_core.
      apply ltb_spec;rewrite H0;compute;trivial.
      intros; repeat (rewrite orb_false_iff in H19);destruct H19. destruct H19.
      unfold Lit.interp in H19.
@@ -1581,7 +1555,7 @@ Transparent build_z_atom.
      unfold Var.interp in H23; rewrite H10 in H23.
      rewrite <-H22, <- H20 in H21.
      assert (t = Typ.TZ).
-       rewrite Typ.eqb_spec in H6; rewrite Typ.eqb_spec in H18; subst; auto.
+       rewrite Typ.eqb_spec in H6; rewrite Typ.eqb_spec in H18; subst; auto with smtcoq_core.
      rewrite H26 in H19.
      case_eq (interp_atom (t_atom .[ b0])); intros t1 v1 Heq1.
      assert (H50: t1 = Typ.TZ).
diff --git a/src/spl/Arithmetic.v b/src/spl/Arithmetic.v
index 05c999d..3f5cd16 100644
--- a/src/spl/Arithmetic.v
+++ b/src/spl/Arithmetic.v
@@ -63,8 +63,6 @@ Section Arith.
     Let wf_rho : Valuation.wf rho.
     Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto. Qed.
 
-    Hint Immediate wf_rho.
-
 
     Lemma valid_check_spl_arith :
       forall orig, C.valid rho orig ->
@@ -76,7 +74,7 @@ Section Arith.
       (* List with one element *)
       intros H res l; case_eq (build_clause Lia.empty_vmap (Lit.neg li :: res :: nil)); [ |intros; apply C.interp_true; auto].
       intros (vm1, bf) Heq; destruct (Lia.build_clause_correct _ _ _ t_func ch_atom ch_form wt_t_atom _ _ _ _ Heq) as [H1 H0].
-      red; simpl; auto.
+      red; simpl; auto with smtcoq_core.
       decompose [and] H0; case_eq (ZTautoChecker bf l); [intros Heq3|intros; apply C.interp_true; auto].
       unfold C.valid; replace (C.interp rho (res :: nil)) with (C.interp rho (Lit.neg li :: res :: nil)).
       rewrite H6; apply ZTautoChecker_sound with l;trivial.
diff --git a/src/spl/Operators.v b/src/spl/Operators.v
index f0aba15..fb3e379 100644
--- a/src/spl/Operators.v
+++ b/src/spl/Operators.v
@@ -279,28 +279,28 @@ intros. destruct H0; now contradict H0.
     Lemma wf_t_form : wf t_form.
     Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[_ H] _]; auto. Qed.
 
-    Local Hint Immediate wf_t_atom default_t_atom default_t_form wf_t_form.
+    Local Hint Immediate wf_t_atom default_t_atom default_t_form wf_t_form : smtcoq_spl_op.
 
     Lemma interp_check_distinct : forall ha diseq,
       check_distinct ha diseq = true ->
       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 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; 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 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; intros i 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); unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite H10; simpl; rewrite Atom.t_interp_wf; auto; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H11: a < length t_atom).
-      case_eq (a < length t_atom); auto; 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; rewrite H4; [exists h2; exists h1|exists h1; exists h2]; auto.
-      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); auto; unfold Lit.interp; replace (Lit.is_pos (diseq .[ i])) with false by (case_eq (Lit.is_pos (diseq .[ i])); auto); unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite H6; simpl; rewrite Atom.t_interp_wf; auto; 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; symmetry; change (is_true (Typ.i_eqb t_i A v1 v1)); rewrite Typ.i_eqb_spec; auto.
+      rewrite distinct_spec; intro H5; symmetry; apply afold_left_andb_true; intros i 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 forallbi_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); auto with smtcoq_spl_op smtcoq_core; 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; intro Heq; generalize H1; rewrite get_outofbound; auto; rewrite default_t_atom; discriminate.
-      unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_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.
+      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 forallbi_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.
 
     Lemma interp_check_distinct_two_args : forall f1 f2,
       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; intro Heq; generalize H1; rewrite get_outofbound; auto; rewrite default_t_form; discriminate); assert (H6: f2 < length t_form) by (case_eq (f2 < length t_form); auto; intro Heq; generalize H2; rewrite get_outofbound; auto; rewrite default_t_form; discriminate); rewrite !Form.t_interp_wf; auto; rewrite H1, H2; simpl; unfold Atom.interp_form_hatom, Atom.interp_hatom; rewrite !Atom.t_interp_wf; auto; rewrite H3, H4; simpl; unfold Atom.wt,is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H7: hb < length t_atom) by (case_eq (hb < length t_atom); auto; intro Heq; generalize H4; rewrite get_outofbound; auto; 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; rewrite Typ.i_eqb_sym; auto.
+      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 forallbi_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.
 
 
@@ -308,13 +308,13 @@ intros. destruct H0; now contradict H0.
     (*   check_distinct ha diseq -> *)
     (*   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; 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); unfold Var.interp; rewrite Form.wf_interp_form; auto; rewrite H5; simpl; rewrite Atom.t_interp_wf; auto; rewrite H6; simpl; unfold Atom.apply_binop; unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_spec in wt_t_atom; assert (H10: a < length t_atom). *)
-  (*     case_eq (a < length t_atom); auto; 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; rewrite H2; [exists h2; exists h1|exists h1; exists h2]; auto. *)
+  (*     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 forallbi_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; intro Heq; generalize H1; rewrite get_outofbound; auto; rewrite default_t_atom; discriminate. *)
-  (*     unfold Atom.wt in wt_t_atom; unfold is_true in wt_t_atom; rewrite forallbi_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. *)
+  (*     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 forallbi_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. *)
 
   End Valid1.
@@ -382,18 +382,18 @@ intros. destruct H0; now contradict H0.
       check_lit l1 l2 -> Lit.interp rho l1 = Lit.interp rho l2.
     Proof.
       unfold check_lit; intros l1 l2; unfold is_true; rewrite !orb_true_iff, !andb_true_iff; intros [[H1|[H1 H2]]|[H1 H2]].
-      rewrite eqb_spec in H1; rewrite H1; auto.
-      rewrite Bool.eqb_true_iff in H1; unfold Lit.interp; rewrite H1, (interp_check_var _ _ H2); auto.
-      generalize H1; unfold Lit.interp; case (Lit.is_pos l1); case (Lit.is_pos l2); try discriminate; intros _; unfold Var.interp; rewrite (interp_check_distinct_two_args _ t_func ch_atom ch_form wt_t_atom _ _ H2); auto; case (rho (Lit.blit l2)); auto.
+      rewrite eqb_spec in H1; rewrite H1; auto with smtcoq_core.
+      rewrite Bool.eqb_true_iff in H1; unfold Lit.interp; rewrite H1, (interp_check_var _ _ H2); auto with smtcoq_core.
+      generalize H1; unfold Lit.interp; case (Lit.is_pos l1); case (Lit.is_pos l2); try discriminate; intros _; unfold Var.interp; rewrite (interp_check_distinct_two_args _ t_func ch_atom ch_form wt_t_atom _ _ H2); auto with smtcoq_core; case (rho (Lit.blit l2)); auto with smtcoq_core.
     Qed.
 
     (* Lemma interp_check_lit : forall l1 l2, *)
     (*   check_lit l1 l2 -> Lit.interp rho l1 -> Lit.interp rho l2 = true. *)
     (* Proof. *)
     (*   unfold check_lit; intros l1 l2; unfold is_true; rewrite !orb_true_iff, !andb_true_iff; intros [[H1|[[H1 H2] H3]]|[[H1 H2] H3]]. *)
-    (*   rewrite Int63Properties.eqb_spec in H1; subst l1; auto. *)
-    (*   unfold Lit.interp; rewrite H1, H2; apply interp_check_var; auto. *)
-    (*   unfold Lit.interp; case_eq (Lit.is_pos l1); intro Heq; rewrite Heq in H1; try discriminate; clear Heq H1; case_eq (Lit.is_pos l2); intro Heq; rewrite Heq in H2; try discriminate; clear Heq H2; case_eq (Var.interp rho (Lit.blit l1)); try discriminate; intros H4 _; case_eq (Var.interp rho (Lit.blit l2)); auto; intro H5; rewrite (interp_check_var _ _ H3 H5) in H4; discriminate. *)
+    (*   rewrite Int63Properties.eqb_spec in H1; subst l1; auto with smtcoq_core. *)
+    (*   unfold Lit.interp; rewrite H1, H2; apply interp_check_var; auto with smtcoq_core. *)
+    (*   unfold Lit.interp; case_eq (Lit.is_pos l1); intro Heq; rewrite Heq in H1; try discriminate; clear Heq H1; case_eq (Lit.is_pos l2); intro Heq; rewrite Heq in H2; try discriminate; clear Heq H2; case_eq (Var.interp rho (Lit.blit l1)); try discriminate; intros H4 _; case_eq (Var.interp rho (Lit.blit l2)); auto with smtcoq_core; intro H5; rewrite (interp_check_var _ _ H3 H5) in H4; discriminate. *)
     (* Qed. *)
 
     (* Local Hint Resolve interp_check_lit. *)
@@ -402,72 +402,72 @@ intros. destruct H0; now contradict H0.
       check_form_aux a b ->
       Form.interp interp_form_hatom interp_form_hatom_bv t_form a = Form.interp interp_form_hatom interp_form_hatom_bv t_form b.
     Proof.
-      intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3|a l1] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3|b m1]; simpl; try discriminate;auto.
+      intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3|a l1] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3|b m1]; simpl; try discriminate;auto with smtcoq_core.
       (* Atom *)
-      unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto.
+      unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto with smtcoq_core.
       (* Interesting case *)
-      apply interp_check_distinct; auto.
+      apply interp_check_distinct; auto with smtcoq_core.
       (* Double negation *)
-      unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; subst j1. rewrite (interp_check_lit _ _ H2). auto.
+      unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; subst j1. rewrite (interp_check_lit _ _ H2). auto with smtcoq_core.
       (* Conjunction *)
-      unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto; intros i Hi; apply interp_check_lit; auto.
+      unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto with smtcoq_core; intros i Hi; apply interp_check_lit; auto with smtcoq_core.
       (* Disjunction *)
-      unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto; intros i Hi; apply interp_check_lit; auto.
+      unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_left_eq; auto with smtcoq_core; intros i Hi; apply interp_check_lit; auto with smtcoq_core.
       (* Implication *)
-      unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_right_eq; auto; intros i Hi; apply interp_check_lit; auto.
+      unfold is_true; rewrite andb_true_iff, eqb_spec, forallbi_spec; intros [H1 H2]; apply afold_right_eq; auto with smtcoq_core; intros i Hi; apply interp_check_lit; auto with smtcoq_core.
       (* Xor *)
-      unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto.
+      unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto with smtcoq_core.
       (* Iff *)
-      unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto.
+      unfold is_true; rewrite andb_true_iff; intros [H1 H2]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2); auto with smtcoq_core.
       (* Ite *)
-      unfold is_true; rewrite !andb_true_iff; intros [[H1 H2] H3]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2), (interp_check_lit _ _ H3); auto.
+      unfold is_true; rewrite !andb_true_iff; intros [[H1 H2] H3]; rewrite (interp_check_lit _ _ H1), (interp_check_lit _ _ H2), (interp_check_lit _ _ H3); auto with smtcoq_core.
     Qed.
 
     (* Lemma interp_check_lit_equiv : forall l1 l2, *)
     (*   check_lit l1 l2 -> check_lit l2 l1 -> *)
     (*   Lit.interp rho l1 = Lit.interp rho l2. *)
     (* Proof. *)
-    (*   intros l1 l2 H1 H2; generalize (interp_check_lit _ _ H1) (interp_check_lit _ _ H2); case (Lit.interp rho l1); case (Lit.interp rho l2); auto; symmetry; auto. *)
+    (*   intros l1 l2 H1 H2; generalize (interp_check_lit _ _ H1) (interp_check_lit _ _ H2); case (Lit.interp rho l1); case (Lit.interp rho l2); auto with smtcoq_core; symmetry; auto with smtcoq_core. *)
     (* Qed. *)
 
     (* Lemma interp_check_form_aux : forall a b, *)
     (*   check_form_aux a b -> *)
     (*   Form.interp interp_form_hatom t_form a -> Form.interp interp_form_hatom t_form b. *)
     (* Proof. *)
-    (*   intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3]; simpl; try discriminate;auto. *)
+    (*   intros [a| | |i1 l1|a1|a1|a1|l1 l2|l1 l2|l1 l2 l3] [b| | |j1 m1|a2|a2|a2|j1 j2|j1 j2|j1 j2 j3]; simpl; try discriminate;auto with smtcoq_core. *)
     (*   (* Atom *) *)
-    (*   unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto. *)
+    (*   unfold is_true; rewrite Int63Properties.eqb_spec; intro; subst a; auto with smtcoq_core. *)
     (*   (* Interesting case *) *)
-    (*   apply interp_check_distinct; auto. *)
+    (*   apply interp_check_distinct; auto with smtcoq_core. *)
     (*   (* Double negation *) *)
     (*   unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; subst j1; apply (fold_ind2 _ _ (fun x y => x = true -> y = true)). *)
-    (*   apply interp_check_lit; auto. *)
-    (*   intros a b; case a; try discriminate; intros H _; rewrite H; auto. *)
+    (*   apply interp_check_lit; auto with smtcoq_core. *)
+    (*   intros a b; case a; try discriminate; intros H _; rewrite H; auto with smtcoq_core. *)
     (*   (* Conjunction *) *)
-    (*   unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite forallbi_spec in H2; intro H3; assert (H4 := afold_left_andb_true_inv _ _ _ H3); clear H3; apply afold_left_andb_true; rewrite <- H1; intros i Hi; eapply interp_check_lit; eauto. *)
+    (*   unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite forallbi_spec in H2; intro H3; assert (H4 := afold_left_andb_true_inv _ _ _ H3); clear H3; apply afold_left_andb_true; rewrite <- H1; intros i Hi; eapply interp_check_lit; eauto with smtcoq_core. *)
     (*   (* Disjunction *) *)
     (*   unfold is_true; rewrite andb_true_iff, Int63Properties.eqb_spec; intros [H1 H2]; rewrite forallbi_spec in H2; intro H3; assert (H4 := afold_left_orb_true_inv _ _ _ H3); clear H3; destruct H4 as [i [H3 H4]]; eapply afold_left_orb_true. *)
-    (*   rewrite <- H1; eauto. *)
-    (*   eapply interp_check_lit; eauto. *)
+    (*   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 forallbi_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. *)
+    (*   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; case_eq (Lit.interp rho (a2 .[ i])); auto; 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; omega. *)
-    (*   generalize (H2 _ H7); rewrite H4; intro H8; rewrite (interp_check_lit _ _ H8 H6) in H5; auto. *)
+    (*   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 (existsbi (fun i l => (i < length a2 - 1) && (negb (Lit.interp rho l))) a2). *)
-    (*   rewrite existsbi_spec; intros [i [_ H5]]; rewrite andb_true_iff in H5; destruct H5 as [H5 H6]; left; exists i; split; auto; generalize H6; case (Lit.interp rho (a2 .[ i])); auto; discriminate. *)
+    (*   rewrite existsbi_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 existsbi_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; discriminate. *)
-    (*   intros H5 _; apply (interp_check_lit _ _ H5); apply H4; auto. *)
+    (*   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 *) *)
-    (*   unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto. *)
+    (*   unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto with smtcoq_core. *)
     (*   (* Iff *) *)
-    (*   unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto. *)
+    (*   unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2), (interp_check_lit_equiv _ _ H3 H4); auto with smtcoq_core. *)
     (*   (* Ite *) *)
-    (*   unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2); case (Lit.interp rho j1); apply interp_check_lit; auto. *)
+    (*   unfold is_true; rewrite !andb_true_iff; intros [[[H1 H2] H3] H4]; rewrite (interp_check_lit_equiv _ _ H1 H2); case (Lit.interp rho j1); apply interp_check_lit; auto with smtcoq_core. *)
     (* Qed. *)
 
   End AUX.
@@ -505,50 +505,46 @@ intros. destruct H0; now contradict H0.
 
 
     Let wf_rho : Valuation.wf rho.
-    Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto. Qed.
+    Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto with smtcoq_core. Qed.
 
     Let default_t_form : default t_form = Ftrue.
-    Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[H _] _]; auto. Qed.
+    Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[H _] _]; auto with smtcoq_core. Qed.
 
     Let wf_t_form : wf t_form.
-    Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[_ H] _]; auto. Qed.
-
-    Local Hint Immediate wf_rho default_t_form wf_t_form.
+    Proof. destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [[_ H] _]; auto with smtcoq_core. Qed.
 
 
     Lemma interp_check_hform : forall h1 h2,
       check_hform h1 h2 -> Var.interp rho h1 = Var.interp rho h2.
     Proof.
       unfold check_hform; apply foldi_down_cont_ind; try discriminate. intros i cont _ _ Hrec h1 h2. unfold is_true; rewrite orb_true_iff; intros [H|H].
-      rewrite Int63Properties.eqb_spec in H; rewrite H; auto.
-      unfold Var.interp; rewrite !wf_interp_form; auto; eapply interp_check_form_aux; eauto.
+      rewrite Int63Properties.eqb_spec in H; rewrite H; auto with smtcoq_core.
+      unfold Var.interp; rewrite !wf_interp_form; auto with smtcoq_core; eapply interp_check_form_aux; eauto with smtcoq_core.
     Qed.
 
-    Local Hint Resolve interp_check_hform.
-
 
     Lemma interp_check_form : forall a b,
       check_form a b ->
       Form.interp interp_form_hatom interp_form_hatom_bv t_form a = Form.interp interp_form_hatom interp_form_hatom_bv t_form b.
-    Proof. apply interp_check_form_aux, interp_check_hform; auto. Qed.
+    Proof. apply interp_check_form_aux, interp_check_hform; auto with smtcoq_core. Qed.
 
 
     Lemma interp_check_lit' : forall l res,
       check_lit' l res -> Lit.interp rho l = Lit.interp rho res.
-    Proof. apply interp_check_lit, interp_check_hform; auto. Qed.
+    Proof. apply interp_check_lit, interp_check_hform; auto with smtcoq_core. Qed.
 
 
     Lemma valid_check_distinct_elim :
       forall input, C.valid rho input ->
         forall res, C.valid rho (check_distinct_elim input res).
     Proof.
-      induction input as [ |l c IHc]; auto; simpl; unfold C.valid; simpl; rewrite orb_true_iff; intros [H|H] res.
+      induction input as [ |l c IHc]; auto with smtcoq_core; simpl; unfold C.valid; simpl; rewrite orb_true_iff; intros [H|H] res.
       case_eq (check_lit' l res); intro Heq; simpl.
-      rewrite <- (interp_check_lit' _ _ Heq), H; auto.
-      rewrite H; auto.
+      rewrite <- (interp_check_lit' _ _ Heq), H; auto with smtcoq_core.
+      rewrite H; auto with smtcoq_core.
       case (check_lit' l res).
-      simpl; rewrite H, orb_true_r; auto.
-      simpl; rewrite (IHc H), orb_true_r; auto.
+      simpl; rewrite H, orb_true_r; auto with smtcoq_core.
+      simpl; rewrite (IHc H), orb_true_r; auto with smtcoq_core.
     Qed.
 
   End Valid.
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v
index e116339..ee0dd96 100644
--- a/src/versions/standard/Array/PArray_standard.v
+++ b/src/versions/standard/Array/PArray_standard.v
@@ -14,6 +14,8 @@
    trees *)
 
 
+Declare Scope array_scope.
+
 Require Import Int31.
 Require Export Int63.
 Require FMapAVL.
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v
index a5a931b..abb91ee 100644
--- a/src/versions/standard/Int63/Int63Native_standard.v
+++ b/src/versions/standard/Int63/Int63Native_standard.v
@@ -20,6 +20,7 @@ Definition size := size.
 
 Notation int := int31.
 
+Declare Scope int63_scope.
 Delimit Scope int63_scope with int.
 Bind Scope int63_scope with int.