diff --git a/coq-vlsm.opam b/coq-vlsm.opam
index 2d377c91..9a0cca0a 100644
--- a/coq-vlsm.opam
+++ b/coq-vlsm.opam
@@ -20,6 +20,7 @@ depends: [
   "coq-stdpp" {>= "1.8.0"}
   "coq-itauto" 
   "coq-equations" 
+  "coq-hammer"
 ]
 
 tags: [
diff --git a/theories/VLSM/Core/Composition.v b/theories/VLSM/Core/Composition.v
index c4397c9d..2349d711 100644
--- a/theories/VLSM/Core/Composition.v
+++ b/theories/VLSM/Core/Composition.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude finite.
 From Coq Require Import Streams FunctionalExtensionality Eqdep_dec.
@@ -398,6 +399,7 @@ Definition lift_to_composite_finite_trace j
 Definition lift_to_composite_finite_trace_last j
   := VLSM_embedding_finite_trace_last (lift_to_composite_VLSM_embedding j).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma constraint_free_incl
   (constraint : composite_label -> composite_state  * option message -> Prop)
   : VLSM_incl (composite_vlsm constraint) free_composite_vlsm.
@@ -1590,6 +1592,7 @@ Definition composite_valid_transition_item
   (s : composite_state IM) (item : composite_transition_item IM) : Prop :=
   CompositeValidTransition (l item) s (input item) (destination item) (output item).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma composite_valid_transition_reachable_iff l s1 iom s2 oom :
   CompositeValidTransition l s1 iom s2 oom <-> ValidTransition RFree l s1 iom s2 oom.
 Proof. by firstorder. Qed.
diff --git a/theories/VLSM/Core/ELMO/BaseELMO.v b/theories/VLSM/Core/ELMO/BaseELMO.v
index e6b71249..ff3aacdc 100644
--- a/theories/VLSM/Core/ELMO/BaseELMO.v
+++ b/theories/VLSM/Core/ELMO/BaseELMO.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude finite.
 From VLSM.Lib Require Import EquationsExtras.
@@ -353,6 +354,7 @@ Proof.
   by split; intros H; decompose [and or ex] H; subst; eauto.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 (**
   When a message belongs to the [sentMessages] of some state, then the state
   contains a corresponding observation which was sent. The converse also holds.
@@ -392,6 +394,7 @@ Proof.
   by destruct (decide (isSend ob)).
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 (**
   When a message belongs to the [receivedMessages] of some state, then the state
   contains a corresponding observation which was received. The converse also holds.
@@ -615,6 +618,7 @@ Proof.
   by apply rec_obs_fn_sizeState.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export] Instance Message_FullMessageDependencies :
   FullMessageDependencies Message_dependencies Message_full_dependencies.
 Proof.
diff --git a/theories/VLSM/Core/ELMO/ELMO.v b/theories/VLSM/Core/ELMO/ELMO.v
index 4592fb80..f6855220 100644
--- a/theories/VLSM/Core/ELMO/ELMO.v
+++ b/theories/VLSM/Core/ELMO/ELMO.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From Coq Require Import FunctionalExtensionality Reals.
 From stdpp Require Import prelude finite.
@@ -329,6 +330,7 @@ Definition ELMOComponent (i : index) : VLSM Message :=
   vmachine := ELMOComponentMachine i;
 |}.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export]
 Instance ComputableSentMessages_ELMOComponent
   (i : index) : ComputableSentMessages (ELMOComponent i).
@@ -344,6 +346,7 @@ Proof.
       by firstorder congruence.
 Defined.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export]
 Instance ComputableReceivedMessages_ELMOComponent
   (i : index) : ComputableReceivedMessages (ELMOComponent i).
@@ -364,6 +367,7 @@ Instance HasBeenDirectlyObservedCapability_ELMOComponent
   (i : index) : HasBeenDirectlyObservedCapability (ELMOComponent i) :=
     HasBeenDirectlyObservedCapability_from_sent_received (ELMOComponent i).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma ELMO_reachable_view (s : State) i :
   ram_state_prop (ELMOComponent i) s
     <->
@@ -588,6 +592,7 @@ Proof.
     intros; apply elem_of_sentMessages_addObservation; constructor; auto.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma local_equivocators_simple_addObservation :
   forall (s : State) (ob : Observation) (a : Address),
     local_equivocators_simple (s <+> ob) a ->
@@ -1262,6 +1267,7 @@ Proof.
     by apply elem_of_receivedMessages, obs_sizeState in Hobs; cbn in Hobs; lia.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 #[export] Instance MessageDependencies_ELMOComponent :
   MessageDependencies Ei Message_dependencies.
 Proof.
diff --git a/theories/VLSM/Core/ELMO/MO.v b/theories/VLSM/Core/ELMO/MO.v
index 7721cb62..1f30659f 100644
--- a/theories/VLSM/Core/ELMO/MO.v
+++ b/theories/VLSM/Core/ELMO/MO.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From Coq Require Import FunctionalExtensionality.
 From stdpp Require Import prelude finite.
@@ -1223,6 +1224,7 @@ Proof.
       by apply rec_recv.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma unfold_rec_obs :
   forall (s : State) (ob : Observation),
     rec_obs s ob
@@ -1232,7 +1234,7 @@ Proof using. clear. (* avoid unneccessary dependence on section variables *)
   intros s ob; split.
   - induction 1.
     + by left; constructor.
-    + by setoid_rewrite elem_of_addObservation; firstorder.
+    + by setoid_rewrite elem_of_addObservation; qauto.
     + by setoid_rewrite elem_of_addObservation; firstorder.
   - induction s using addObservation_ind.
     + by firstorder using elem_of_nil.
diff --git a/theories/VLSM/Core/ELMO/UMO.v b/theories/VLSM/Core/ELMO/UMO.v
index 7aaaa081..b5c0306b 100644
--- a/theories/VLSM/Core/ELMO/UMO.v
+++ b/theories/VLSM/Core/ELMO/UMO.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From Coq Require Import FunctionalExtensionality.
 From stdpp Require Import prelude finite.
@@ -114,10 +115,10 @@ Proof.
   - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
     destruct l, im; cbn in *; invert_UMOComponentValid
     ; inversion Ht; subst; clear Ht; cbn.
-    + by rewrite decide_False; cbn; firstorder congruence.
+    + by rewrite decide_False; cbn; qauto; congruence.
     + rewrite decide_True by done; cbn.
       unfold Message; rewrite elem_of_cons.
-      by firstorder congruence.
+      by qauto; congruence.
 Defined.
 
 #[export]
@@ -132,8 +133,8 @@ Proof.
     ; inversion Ht; subst; clear Ht; cbn.
     + rewrite decide_True by done; cbn.
       unfold Message; rewrite elem_of_cons.
-      by firstorder congruence.
-    + by rewrite decide_False; cbn; firstorder congruence.
+      by qauto; congruence.
+    + by rewrite decide_False; cbn; qauto; congruence.
 Defined.
 
 #[export]
@@ -1408,14 +1409,14 @@ Instance sent_comparable_dec : RelDecision sent_comparable.
 Proof.
   intros m1 m2.
   destruct (decide (adr (state m1) = adr (state m2)));
-    [| by right; destruct 1; apply n; firstorder congruence].
+    [| by right; destruct 1; apply n; qauto; congruence].
   destruct (decide (obs (state m1) = obs (state m2)));
     [by left; replace m2 with m1 by (apply eq_Message; done); constructor |].
   destruct (decide (m1 ∈ sentMessages (state m2)));
     [by left; constructor; constructor |].
   destruct (decide (m2 ∈ sentMessages (state m1)));
     [by left; constructor; constructor |].
-  by right; destruct 1; firstorder.
+  by right; destruct 1; qauto.
 Defined.
 
 #[export]
diff --git a/theories/VLSM/Core/Equivocation/NoEquivocation.v b/theories/VLSM/Core/Equivocation/NoEquivocation.v
index 3b89a5d7..f82c101f 100644
--- a/theories/VLSM/Core/Equivocation/NoEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/NoEquivocation.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation.
@@ -132,7 +133,7 @@ Proof.
     split; [| done].
     rapply extend_right_finite_trace_from; [done |].
     apply finite_valid_trace_last_pstate in IHtr as Hs.
-    cut (option_valid_message_prop X iom); [by firstorder |].
+    cut (option_valid_message_prop X iom); [by hauto|].
     destruct iom as [m |]; [| by apply option_valid_message_None].
     destruct Hx as [Hv _].
     apply Henforced in Hv.
diff --git a/theories/VLSM/Core/VLSM.v b/theories/VLSM/Core/VLSM.v
index a7a16f7c..60db89fd 100644
--- a/theories/VLSM/Core/VLSM.v
+++ b/theories/VLSM/Core/VLSM.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From Coq Require Import Streams.
@@ -165,7 +166,7 @@ Lemma trace_has_message_observed_iff m tr
   (Hobserved : trace_has_message item_sends_or_receives m tr)
   : trace_has_message (field_selector input) m tr \/ trace_has_message (field_selector output) m tr.
 Proof.
-  by unfold trace_has_message in *; rewrite !Exists_exists in *; firstorder.
+  by unfold trace_has_message in *; rewrite !Exists_exists in *; qauto.
 Qed.
 
 (** Defines a message received but not sent by within the trace. *)
@@ -790,7 +791,7 @@ Proof.
   split.
   - intros Hm; inversion Hm; subst.
     + by right.
-    + by left; exists (s1, om0), l0; firstorder.
+    + by left; exists (s1, om0), l0; strivial.
   - intros [Hem | Him].
     + by apply option_can_produce_valid.
     + by constructor; apply Him.
@@ -870,7 +871,7 @@ Proof.
   - intro Hps'. destruct Hps' as [om' Hs].
     inversion Hs; subst.
     + by left; exists (exist _ _ Hs0).
-    + by right; exists l0, (s, om), om'; firstorder.
+    + by right; exists l0, (s, om), om'; strivial.
   - intros [[[s His] Heq] | [l [[s om] [om' [[[_om Hps] [[_s Hpm] Hv]] Ht]]]]]; subst.
     + by exists None; apply valid_initial_state_message.
     + by exists om'; apply valid_generated_state_message with s _om _s om l.
@@ -898,7 +899,7 @@ Proof.
   destruct Hs as [om Hs].
   induction Hs.
   - by apply IHinit.
-  - by apply (IHgen s' l0 om om' s); firstorder.
+  - by apply (IHgen s' l0 om om' s); strivial.
 Qed.
 
 (** Valid message characterization. *)
@@ -913,7 +914,7 @@ Proof.
   - intros [s' Hpm'].
     inversion Hpm'; subst.
     + by left; exists (exist _ m' Hom).
-    + by right; exists l0, (s, om), s'; firstorder.
+    + by right; exists l0, (s, om), s'; strivial.
   - intros [[[s His] Heq] | [l [[s om] [s' [[[_om Hps] [[_s Hpm] Hv]] Ht]]]]]; subst.
     + by apply initial_message_is_valid.
     + by exists s'; apply valid_generated_state_message with s _om _s om l.
@@ -1634,7 +1635,7 @@ Proof.
     apply finite_valid_trace_from_to_singleton.
     apply finite_valid_trace_init_to_emit_valid_state_message in Htl1.
     apply finite_valid_trace_init_to_emit_valid_state_message in Htl2.
-    by firstorder.
+    by strivial.
 Qed.
 
 Lemma finite_valid_trace_init_to_add_emit
@@ -1684,7 +1685,7 @@ Proof.
     {
       apply finite_valid_trace_init_to_emit_valid_state_message in Htr1.
       apply finite_valid_trace_init_to_emit_valid_state_message in Htr2.
-      by firstorder.
+      by strivial.
     }
     apply finite_valid_trace_init_to_emit_output in Htr2 as Houtput.
     apply finite_valid_trace_init_to_emit_forget_emit in Htr1.
@@ -1961,7 +1962,7 @@ Proof.
   apply finite_valid_trace_from_to_last in Htrs as Hlast.
   rewrite <- Hlast in Htr.
   apply finite_valid_trace_from_to_forget_last in Htrs.
-  by firstorder using finite_valid_trace_from_app_iff.
+  by strivial using finite_valid_trace_from_app_iff.
 Qed.
 
 (**
@@ -2807,7 +2808,7 @@ Context
 Lemma ValidTransition_preloaded_iff :
   forall l s1 iom s2 oom,
     ValidTransition X l s1 iom s2 oom <-> ValidTransition R l s1 iom s2 oom.
-Proof. by firstorder. Qed.
+Proof. by sauto. Qed.
 
 Lemma ValidTransitionNext_preloaded_iff :
   forall s1 s2, ValidTransitionNext X s1 s2 <-> ValidTransitionNext R s1 s2.
@@ -2824,7 +2825,7 @@ Lemma input_valid_transition_forget_input :
   forall l s1 iom s2 oom,
     input_valid_transition X l (s1, iom) (s2, oom) ->
     ValidTransition X l s1 iom s2 oom.
-Proof. by firstorder. Qed.
+Proof. by hauto. Qed.
 
 End sec_valid_transition_props.
 
diff --git a/theories/VLSM/Core/VLSMProjections/VLSMEquality.v b/theories/VLSM/Core/VLSMProjections/VLSMEquality.v
index 20caf4a3..f05be926 100644
--- a/theories/VLSM/Core/VLSMProjections/VLSMEquality.v
+++ b/theories/VLSM/Core/VLSMProjections/VLSMEquality.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections.VLSMInclusion VLSMProjections.VLSMEmbedding.
@@ -41,6 +42,7 @@ Proof.
   by intros Heq t Hyt; apply Heq.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_incl_iff
   (MX MY : VLSMMachine vtype)
   (X := mk_vlsm MX) (Y := mk_vlsm MY)
@@ -51,6 +53,7 @@ End sec_VLSM_equality.
 
 Notation VLSM_eq X Y := (VLSM_eq_part (machine X) (machine Y)).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_refl
   {message : Type}
   {vtype : VLSMType message}
@@ -61,6 +64,7 @@ Proof.
   by firstorder.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_sym
   {message : Type}
   {vtype : VLSMType message}
@@ -71,6 +75,7 @@ Proof.
   by firstorder.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_eq_trans
   {message : Type}
   {vtype : VLSMType message}
diff --git a/theories/VLSM/Core/VLSMProjections/VLSMInclusion.v b/theories/VLSM/Core/VLSMProjections/VLSMInclusion.v
index ba7e4bb0..4e2647c5 100644
--- a/theories/VLSM/Core/VLSMProjections/VLSMInclusion.v
+++ b/theories/VLSM/Core/VLSMProjections/VLSMInclusion.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections.VLSMEmbedding VLSMProjections.VLSMTotalProjection.
@@ -24,6 +25,7 @@ Definition VLSM_incl_part
     valid_trace_prop X t -> valid_trace_prop Y t.
 #[local] Notation VLSM_incl X Y := (VLSM_incl_part (machine X) (machine Y)).
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_incl_refl
   (MX : VLSMMachine vtype)
   (X := mk_vlsm MX)
@@ -32,6 +34,7 @@ Proof.
   by firstorder.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma VLSM_incl_trans
   (MX MY MZ : VLSMMachine vtype)
   (X := mk_vlsm MX) (Y := mk_vlsm MY) (Z := mk_vlsm MZ)
diff --git a/theories/VLSM/Core/Validator.v b/theories/VLSM/Core/Validator.v
index a8ef9e51..78d73935 100644
--- a/theories/VLSM/Core/Validator.v
+++ b/theories/VLSM/Core/Validator.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections Composition.
@@ -587,7 +588,7 @@ Proof.
         (VLSM_projection_input_valid_transition Hproji); [done |].
       by split; [| apply injective_projections].
     + assert (HivtX : input_valid_transition X lX (sX, om) (vtransition X lX (sX, om)))
-        by firstorder.
+        by strivial.
       destruct (vtransition _ _ _) as (sX', _om').
       eapply (VLSM_projection_input_valid_transition Hproj) in HivtX as [_ Hs']; [| done].
       rewrite HsX in Hs'.
diff --git a/theories/VLSM/Lib/FinSetExtras.v b/theories/VLSM/Lib/FinSetExtras.v
index b19e3c1b..4a09d985 100644
--- a/theories/VLSM/Lib/FinSetExtras.v
+++ b/theories/VLSM/Lib/FinSetExtras.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
@@ -195,7 +196,7 @@ Proof.
   intros a Ha.
   apply elem_of_map in Ha.
   apply elem_of_map.
-  by firstorder.
+  by strivial.
 Qed.
 
 Lemma set_map_size_upper_bound
diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v
index cc660e41..79fde75f 100644
--- a/theories/VLSM/Lib/ListExtras.v
+++ b/theories/VLSM/Lib/ListExtras.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import finite.
 From Coq Require Import FinFun.
@@ -884,7 +885,7 @@ Lemma nth_error_map
   (n : nat)
   : nth_error (List.map f l) n = option_map f (nth_error l n).
 Proof.
-  by revert n; induction l; intros [| n]; firstorder.
+  by revert n; induction l; intros [| n]; strivial.
 Qed.
 
 Lemma exists_finite
@@ -960,6 +961,7 @@ Proof.
   by destruct (f a); cbn; congruence.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma map_option_nth
   {A B : Type}
   (f : A -> option B)
@@ -1437,8 +1439,8 @@ Proof.
   induction 2; cbn.
   - apply PeanoNat.Nat.add_lt_le_mono; [done |].
     induction l; cbn; [done |].
-    by apply PeanoNat.Nat.add_le_mono; firstorder.
-  - by apply PeanoNat.Nat.add_le_lt_mono; firstorder.
+    by apply PeanoNat.Nat.add_le_mono; qauto.
+  - by apply PeanoNat.Nat.add_le_lt_mono; strivial.
 Qed.
 
 (**
diff --git a/theories/VLSM/Lib/ListSetExtras.v b/theories/VLSM/Lib/ListSetExtras.v
index 2d8f5cdd..902302d2 100644
--- a/theories/VLSM/Lib/ListSetExtras.v
+++ b/theories/VLSM/Lib/ListSetExtras.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble ListExtras StdppExtras StdppListSet.
@@ -17,7 +18,7 @@ Lemma set_eq_extract_forall
   (l1 l2 : set A)
   : set_eq l1 l2 <-> forall a, (a ∈ l1 <-> a ∈ l2).
 Proof.
-  by unfold set_eq; firstorder.
+  by unfold set_eq; strivial.
 Qed.
 
 Lemma set_eq_fin_set `{FinSet A Cm} (s1 s2 : Cm) :
@@ -48,7 +49,7 @@ Qed.
 Lemma set_eq_comm {A} : forall s1 s2 : set A,
   set_eq s1 s2 <-> set_eq s2 s1.
 Proof.
-  by firstorder.
+  by qauto.
 Qed.
 
 Lemma set_eq_tran {A} : forall s1 s2 s3 : set A,
@@ -56,7 +57,7 @@ Lemma set_eq_tran {A} : forall s1 s2 s3 : set A,
   set_eq s2 s3 ->
   set_eq s1 s3.
 Proof.
-  by intros; split; apply PreOrder_Transitive with s2; firstorder.
+  by intros; split; apply PreOrder_Transitive with s2; qauto.
 Qed.
 
 Lemma set_eq_empty_iff
@@ -78,9 +79,10 @@ Proof.
   intros a s1 s2 Heq.
   rewrite !set_eq_extract_forall in *.
   setoid_rewrite elem_of_cons.
-  by firstorder.
+  by qauto.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma set_eq_Forall
   {A : Type}
   (s1 s2 : set A)
@@ -132,7 +134,7 @@ Proof.
   intros.
   unfold subseteq, list_subseteq.
   setoid_rewrite set_union_iff.
-  by firstorder.
+  by qauto.
 Qed.
 
 Lemma set_union_iterated_nodup `{EqDecision A}
@@ -336,7 +338,7 @@ Proof.
   - by cbn in H; rewrite decide_True in H; constructor.
   - rewrite elem_of_cons in H0.
     simpl in H; rewrite decide_False in H by done; inversion H; subst; clear H.
-    constructor; [| by firstorder].
+    constructor; [| by strivial].
     by intro Ha; apply (set_remove_3 _ x) in Ha; auto.
 Qed.
 
@@ -646,6 +648,7 @@ Proof.
   by intros a l1 l2 H; split; apply H.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Add Parametric Morphism A : (@elem_of_list A)
   with signature @eq A ==> @list_subseteq A ==> Basics.impl as set_elem_of_subseteq.
 Proof. by firstorder. Qed.
diff --git a/theories/VLSM/Lib/Preamble.v b/theories/VLSM/Lib/Preamble.v
index 2f462125..931ad3f0 100644
--- a/theories/VLSM/Lib/Preamble.v
+++ b/theories/VLSM/Lib/Preamble.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Coq Require Export Program.Tactics.
 Obligation Tactic := idtac.
 From stdpp Require Import prelude.
@@ -20,21 +21,21 @@ Proof.
 Qed.
 
 Lemma and_proper_l (A B C : Prop) : (A -> (B <-> C)) -> (A /\ B) <-> (A /\ C).
-Proof. by firstorder. Qed.
+Proof. by strivial. Qed.
 
 Lemma impl_proper (A B C : Prop) : (A -> (B <-> C)) -> (A -> B) <-> (A -> C).
-Proof. by firstorder. Qed.
+Proof. by strivial. Qed.
 
 (** ** Decidable propositions *)
 
 Lemma Decision_iff : forall {P Q}, (P <-> Q) -> Decision P -> Decision Q.
-Proof. by firstorder. Qed.
+Proof. by qauto. Qed.
 Lemma Decision_and : forall {P Q}, Decision P -> Decision Q -> Decision (P /\ Q).
-Proof. by firstorder. Qed.
+Proof. by qauto. Qed.
 Lemma Decision_or : forall {P Q}, Decision P -> Decision Q -> Decision (P \/ Q).
-Proof. by firstorder. Qed.
+Proof. by qauto. Qed.
 Lemma Decision_not : forall {P}, Decision P -> Decision (~ P).
-Proof. by firstorder. Qed.
+Proof. by qauto. Qed.
 
 #[export] Instance bool_decision {b : bool} : Decision b :=
 match b with
@@ -63,7 +64,7 @@ Lemma tc_reflect
   (P : A -> Prop)
   (Hreflects : forall dm m, R dm m -> P m -> P dm)
   : forall dm m, tc R dm m -> P m -> P dm.
-Proof. by induction 1; firstorder. Qed.
+Proof. by induction 1; strivial. Qed.
 
 (** Characterization of [tc] in terms of the last transitivity step. *)
 Lemma tc_r_iff `(R : relation A) :
@@ -278,7 +279,7 @@ Lemma asymmetric_minimal_among_iff
   : forall m, minimal_among R P m <-> strict_minimal_among R P m.
 Proof.
   unfold minimal_among, strict_minimal_among; specialize asymmetry.
-  by firstorder.
+  by hauto.
 Qed.
 
 (** The minimality definitions are equivalent for [StrictOrder]s. *)
@@ -345,7 +346,7 @@ Lemma compare_asymmetric' {A} `{CompareAsymmetric A} :
 Proof.
   intros x y.
   rewrite compare_asymmetric.
-  by destruct (compare y x); cbn; firstorder congruence.
+  by destruct (compare y x); cbn; strivial; congruence.
 Qed.
 
 (** Strictly-ordered comparisons are asymmetric. *)
@@ -511,7 +512,7 @@ Lemma option_compare_reflexive
   (X : Type) `{StrictlyComparable X}
   : CompareReflexive (option_compare X).
 Proof.
-  by intros [x |] [y |]; cbn; rewrite ?compare_eq; firstorder congruence.
+  by intros [x |] [y |]; cbn; rewrite ?compare_eq; strivial; congruence.
 Qed.
 
 Lemma option_compare_transitive
diff --git a/theories/VLSM/Lib/SortedLists.v b/theories/VLSM/Lib/SortedLists.v
index 54766e2a..db089d7f 100644
--- a/theories/VLSM/Lib/SortedLists.v
+++ b/theories/VLSM/Lib/SortedLists.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From Coq Require Import Sorting.
@@ -194,7 +195,7 @@ Proof.
   intros x y s LS IN. revert y x LS IN.
   induction s.
   - by inversion 2.
-  - by do 2 inversion 1; subst; firstorder.
+  - by do 2 inversion 1; subst; sauto.
 Qed.
 
 Lemma add_in_sorted_list_existing
diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v
index 6f8253de..3fd92a02 100644
--- a/theories/VLSM/Lib/StdppExtras.v
+++ b/theories/VLSM/Lib/StdppExtras.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble ListExtras.
@@ -192,7 +193,7 @@ Proof.
   - by rewrite 2 filter_nil.
   - rewrite 2 filter_cons.
     setoid_rewrite elem_of_cons in H1.
-    by destruct (decide (P a)), (decide (Q a)); [rewrite IHl | ..]; firstorder.
+    by destruct (decide (P a)), (decide (Q a)); [rewrite IHl | ..]; qauto.
 Qed.
 
 Lemma ext_elem_of_filter {A} P Q
@@ -232,8 +233,8 @@ Proof.
   apply NoDup_cons in Hnda.
   setoid_rewrite elem_of_cons in Ha.
   destruct Hnda as [Ha' Hnd']; split.
-  - by apply NoDup_app; firstorder.
-  - by rewrite elem_of_app; firstorder.
+  - by apply NoDup_app; qauto.
+  - by rewrite elem_of_app; qauto.
 Qed.
 
 Lemma list_lookup_lt [A] (is : list A) :
@@ -513,6 +514,7 @@ Proof.
   by induction 1; cbn; rewrite elem_of_cons, dsig_eq; cbn; auto.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma elem_of_map_option
   {A B : Type}
   (f : A -> option B)
@@ -598,7 +600,7 @@ Lemma map_option_subseteq
   (Hincl : l1 ⊆ l2)
   : map_option f l1 ⊆ map_option f l2.
 Proof.
-  by intros b; rewrite !elem_of_map_option; firstorder.
+  by intros b; rewrite !elem_of_map_option; strivial.
 Qed.
 
 Lemma elem_of_cat_option
@@ -626,7 +628,7 @@ Lemma map_option_incl
   (Hincl : incl l1 l2)
   : incl (map_option f l1) (map_option f l2).
 Proof.
-  by intros b; rewrite !in_map_option; firstorder.
+  by intros b; rewrite !in_map_option; strivial.
 Qed.
 
 Lemma list_max_elem_of_exists2
diff --git a/theories/VLSM/Lib/StdppListSet.v b/theories/VLSM/Lib/StdppListSet.v
index e3b7606e..1c4339ad 100644
--- a/theories/VLSM/Lib/StdppListSet.v
+++ b/theories/VLSM/Lib/StdppListSet.v
@@ -1,4 +1,5 @@
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
+From Hammer Require Import Tactics.
 From stdpp Require Import prelude.
 
 Section sec_fst_defs.
@@ -102,7 +103,7 @@ Proof.
   inversion_clear Hnd.
   destruct (decide (b = x)) as [<- | Hbx].
   - by intros Ha ->.
-  - by rewrite elem_of_cons; firstorder subst.
+  - by rewrite elem_of_cons; qauto; subst.
 Qed.
 
 Lemma set_remove_3 (a b : A) (l : set) :
@@ -167,7 +168,7 @@ Lemma set_diff_intro :
 Proof.
   induction x; cbn; [by inversion 1 |].
   by intros y; destruct (decide (a0 ∈ y));
-    rewrite elem_of_cons, ?set_add_iff; firstorder congruence.
+    rewrite elem_of_cons, ?set_add_iff; qauto; congruence.
 Qed.
 
 Lemma set_diff_elim1 :
@@ -175,14 +176,14 @@ Lemma set_diff_elim1 :
     a ∈ set_diff x y -> a ∈ x.
 Proof.
   induction x; cbn; [done |]; intros y.
-  by destruct (decide (a0 ∈ y)); rewrite elem_of_cons, ?set_add_iff; firstorder.
+  by destruct (decide (a0 ∈ y)); rewrite elem_of_cons, ?set_add_iff; qauto.
 Qed.
 
 Lemma set_diff_elim2 :
   forall (a : A) (x y : set), a ∈ set_diff x y -> a ∉ y.
 Proof.
   induction x; cbn; [by inversion 1 |].
-  by intros y; destruct (decide (a0 ∈ y)); rewrite ?set_add_iff; firstorder congruence.
+  by intros y; destruct (decide (a0 ∈ y)); rewrite ?set_add_iff; qauto; congruence.
 Qed.
 
 Lemma set_diff_iff a l l' :
diff --git a/theories/VLSM/Lib/StreamExtras.v b/theories/VLSM/Lib/StreamExtras.v
index 775f33b0..7d4141cd 100644
--- a/theories/VLSM/Lib/StreamExtras.v
+++ b/theories/VLSM/Lib/StreamExtras.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From stdpp Require Import prelude.
 From Coq Require Import Streams Sorted.
 From VLSM.Lib Require Import Preamble ListExtras StdppExtras SortedLists NeList.
@@ -724,7 +725,7 @@ Proof.
   intros [a s] H.
   inversion H. simpl in H1. apply IH in H1.
   constructor; [| done].
-  by rewrite Exists1_exists in *; firstorder.
+  by rewrite Exists1_exists in *; strivial.
 Qed.
 
 Lemma FinitelyManyBound_impl_rev
@@ -735,7 +736,7 @@ Proof.
   exists n.
   apply ForAll1_forall.
   rewrite ForAll1_forall in Hn.
-  by firstorder.
+  by qauto.
 Qed.
 
 Definition stream_prepend {A} (nel : ne_list A) (s : Stream A) : Stream A :=
diff --git a/theories/VLSM/Lib/Temporal.v b/theories/VLSM/Lib/Temporal.v
index 71afdcdd..4fe38b08 100644
--- a/theories/VLSM/Lib/Temporal.v
+++ b/theories/VLSM/Lib/Temporal.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From Coq Require Import Streams Classical.
@@ -137,6 +138,7 @@ Proof.
   by intro; apply Classical_Prop.NNPP.
 Qed.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma stabilization [A : Type] [R : A -> A-> Prop] (HR : well_founded R)
       [s] : progress R s -> exists x, Eventually (Forever (fun s => hd s = x)) s.
 Proof.
diff --git a/theories/VLSM/Lib/TopSort.v b/theories/VLSM/Lib/TopSort.v
index 2db40099..82df716f 100644
--- a/theories/VLSM/Lib/TopSort.v
+++ b/theories/VLSM/Lib/TopSort.v
@@ -1,3 +1,4 @@
+From Hammer Require Import Tactics.
 From Cdcl Require Import Itauto. #[local] Tactic Notation "itauto" := itauto auto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble ListExtras ListSetExtras StdppListSet StdppExtras.
@@ -384,6 +385,7 @@ Definition precedes_closed
   :=
   Forall (fun (b : A) => forall (a : A) (Hmj : precedes a b), a ∈ s) s.
 
+(* Replacing firstorder with sauto might cause it to get stuck *)
 Lemma precedes_closed_set_eq
   {A : Type}
   (precedes : relation A)