diff --git a/searchAndDestroy.sh b/searchAndDestroy.sh
new file mode 100755
index 00000000..b8684358
--- /dev/null
+++ b/searchAndDestroy.sh
@@ -0,0 +1,23 @@
+for file in `find theories/VLSM/Core/ELMO/ -maxdepth 1 -name '*.v'`; do
+   fline=`cat $file | head -n1`
+   if [[ $fline == 'Set Default Proof Using "Type".' ]]; then
+      echo $file
+      echo "already parsed"
+   else
+      echo $file
+      echo -e "Set Default Proof Using \"Type\".\n$(cat $file)" > $file
+      OUTPUT=`make "${file}o" 2>&1 1>/dev/null`
+      while [[ `echo $OUTPUT | wc -w` > 0 ]]; do
+         echo "try again"
+         ADD="Proof using "`echo -e $OUTPUT | grep -o -E "but not declared: [, _[:alnum:]]*\." | sed 's/but not declared: //'`
+         LINE=`echo $OUTPUT | grep "line.*characters.*" | cut -d' ' -f4 | cut -d',' -f1`
+         PLINE=`cat $file | head -n $LINE | grep -n "Proof\." | tail -n -1 | cut -d':' -f1`
+         echo $PLINE
+         cat $file | head -n $PLINE | tail -n -1
+         sed -i "${PLINE}s/Proof\./${ADD}/" $file
+         cat $file | head -n $PLINE | tail -n -1
+         OUTPUT=`make "${file}o" 2>&1 1>/dev/null`
+      done
+   fi
+done
+
diff --git a/theories/VLSM/Core/AnnotatedVLSM.v b/theories/VLSM/Core/AnnotatedVLSM.v
index f8d05b97..c47349e0 100644
--- a/theories/VLSM/Core/AnnotatedVLSM.v
+++ b/theories/VLSM/Core/AnnotatedVLSM.v
@@ -3,6 +3,8 @@ From stdpp Require Import prelude.
 From VLSM.Lib Require Import ListExtras.
 From VLSM.Core Require Import VLSM VLSMProjections Validator Composition.
 
+Set Default Proof Using "Type".
+
 (** * State-annotated VLSMs
 
   This module describes the VLSM obtained by augmenting the states of an existing
diff --git a/theories/VLSM/Core/ByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces.v
index 6943ef2e..97a3f005 100644
--- a/theories/VLSM/Core/ByzantineTraces.v
+++ b/theories/VLSM/Core/ByzantineTraces.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM VLSMProjections Composition ProjectionTraces Validator.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Byzantine Traces
 
   In this section, we introduce two definitions of Byzantine traces,
@@ -359,7 +361,7 @@ Context
 *)
 Lemma validator_pre_loaded_with_all_messages_incl
     : VLSM_incl PreLoadedX X.
-Proof.
+Proof using Hvalidator.
   apply VLSM_incl_finite_traces_characterization.
   intros.
   split; [| by apply H].
@@ -395,7 +397,7 @@ Lemma composite_validator_byzantine_traces_are_not_byzantine
     (tr : vTrace X)
     (Hbyz : byzantine_trace_prop X tr)
     : valid_trace_prop X tr.
-Proof.
+Proof using Hvalidator.
   apply validator_pre_loaded_with_all_messages_incl.
   apply alt_pre_loaded_with_all_messages_incl.
   by apply byzantine_alt_byzantine_iff in Hbyz.
diff --git a/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v
index e12a82ea..fd69ee02 100644
--- a/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v
+++ b/theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v
@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude finite.
 From Coq Require Import FunctionalExtensionality.
@@ -94,7 +95,7 @@ Definition fixed_byzantine_IM : index -> VLSM message :=
 
 Lemma fixed_byzantine_IM_no_initial_messages
   : forall i m, ~ vinitial_message_prop (fixed_byzantine_IM i) m.
-Proof.
+Proof using no_initial_messages_in_IM.
   unfold fixed_byzantine_IM, update_IM. simpl.
   intros i m Hm.
   by case_decide; [| destruct (no_initial_messages_in_IM i m)].
@@ -102,7 +103,7 @@ Qed.
 
 Lemma fixed_byzantine_IM_preserves_channel_authentication
 : channel_authentication_prop fixed_byzantine_IM A sender.
-Proof.
+Proof using can_emit_signed.
   unfold fixed_byzantine_IM, update_IM. simpl.
   intros i m Hm.
   case_decide; [| by apply can_emit_signed].
@@ -122,7 +123,7 @@ Definition message_as_byzantine_label
   (i : index)
   (Hi : i ∈ byzantine)
   : composite_label fixed_byzantine_IM.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   exists i.
   unfold fixed_byzantine_IM, update_IM.
   simpl.
@@ -272,7 +273,7 @@ Definition pre_loaded_fixed_non_byzantine_vlsm : VLSM message :=
 
 Lemma non_byzantine_nodes_same
   : forall sub_i, sub_IM fixed_byzantine_IM (elements non_byzantine) sub_i = sub_IM IM (elements non_byzantine) sub_i.
-Proof.
+Proof using H6 H3 H.
   intro sub_i.
   destruct_dec_sig sub_i i Hi Heqsub_i.
   subst.
@@ -284,7 +285,7 @@ Qed.
 
 Lemma non_byzantine_nodes_same_sym
   : forall sub_i, sub_IM IM (elements non_byzantine) sub_i = sub_IM fixed_byzantine_IM (elements non_byzantine) sub_i.
-Proof.
+Proof using H6 H3 H.
   by intro; symmetry; apply non_byzantine_nodes_same.
 Qed.
 
@@ -331,7 +332,7 @@ Lemma fixed_non_byzantine_projection_valid_no_equivocations
       (sub_IM fixed_byzantine_IM (elements non_byzantine))
       fixed_set_signed_message
       l (s, om).
-Proof.
+Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety.
   intros l s om Hv.
   apply
     (sub_IM_no_equivocation_preservation fixed_byzantine_IM (elements non_byzantine)
@@ -354,7 +355,7 @@ Qed.
 
 Lemma fixed_non_byzantine_pre_loaded_incl
   : VLSM_incl fixed_non_byzantine_projection pre_loaded_fixed_non_byzantine_vlsm'.
-Proof.
+Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety.
   apply basic_VLSM_incl.
   - by intro; intros; apply fixed_non_byzantine_projection_initial_state_preservation.
   - intros l s m (Hs & _ & Hv) HsY _.
@@ -377,7 +378,7 @@ Lemma pre_loaded_fixed_non_byzantine_vlsm_lift_valid
        non_byzantine_not_equivocating_constraint)
     (lift_sub_label fixed_byzantine_IM (elements non_byzantine))
     (lift_sub_state fixed_byzantine_IM (elements non_byzantine)).
-Proof.
+Proof using can_emit_signed Hsender_safety.
   intros (sub_i, li) s om (HsX & HomX & Hv & Hc & _) HsY HomY.
   destruct_dec_sig sub_i i Hi Heqsub_i; subst.
   split; [by apply lift_sub_valid |].
@@ -406,7 +407,7 @@ Lemma pre_loaded_fixed_non_byzantine_vlsm_lift_initial_message
     (composite_vlsm fixed_byzantine_IM
        non_byzantine_not_equivocating_constraint)
     (lift_sub_state fixed_byzantine_IM (elements non_byzantine)).
-Proof.
+Proof using no_initial_messages_in_IM.
   intros l s m Hv HsY HmX.
   destruct HmX as [[sub_i [[im Him] Heqm]] | Hseeded].
   - exfalso. clear -no_initial_messages_in_IM Him.
@@ -461,7 +462,7 @@ Lemma pre_loaded_fixed_non_byzantine_vlsm_lift :
     (composite_vlsm fixed_byzantine_IM non_byzantine_not_equivocating_constraint)
     (lift_sub_label fixed_byzantine_IM (elements non_byzantine))
     (lift_sub_state fixed_byzantine_IM (elements non_byzantine)).
-Proof.
+Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety.
   apply basic_VLSM_embedding.
   - by intro; intros; apply pre_loaded_fixed_non_byzantine_vlsm_lift_valid.
   - by intro; intros * []; rapply lift_sub_transition.
@@ -471,7 +472,7 @@ Qed.
 
 Lemma pre_loaded_fixed_non_byzantine_incl
   : VLSM_incl pre_loaded_fixed_non_byzantine_vlsm' fixed_non_byzantine_projection.
-Proof.
+Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety.
   apply basic_VLSM_incl; cbn.
   - by intro; intros; apply fixed_non_byzantine_projection_initial_state_preservation.
   - by intros l s m Hv _ Him; apply initial_message_is_valid.
@@ -487,7 +488,7 @@ Qed.
 
 Lemma fixed_non_byzantine_pre_loaded_eq
   : VLSM_eq fixed_non_byzantine_projection pre_loaded_fixed_non_byzantine_vlsm'.
-Proof.
+Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety.
   apply VLSM_eq_incl_iff. split.
   - by apply fixed_non_byzantine_pre_loaded_incl.
   - by apply pre_loaded_fixed_non_byzantine_incl.
@@ -551,7 +552,7 @@ Lemma fixed_non_equivocating_incl_sub_non_equivocating
       (pre_induced_sub_projection IM (elements selection_complement)
         (sub_IM_not_equivocating_constraint IM
           (elements selection_complement) A sender)).
-Proof.
+Proof using can_emit_signed Hsender_safety H6 H3 H.
   apply induced_sub_projection_constraint_subsumption_incl.
   intros l (s, om) Hv.
   apply (fixed_strong_equivocation_subsumption IM selection)
@@ -580,7 +581,7 @@ Qed.
 
 Lemma fixed_non_equivocating_incl_fixed_non_byzantine
   : VLSM_incl FixedNonEquivocating PreNonByzantine.
-Proof.
+Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety H6 H3.
   apply basic_VLSM_incl.
   - intros s (sX & <- & Hinitial) sub_i.
     by apply Hinitial.
@@ -622,7 +623,7 @@ Qed.
 Corollary fixed_equivocating_traces_are_byzantine is tr
   : finite_valid_trace Fixed is tr ->
     fixed_byzantine_trace_alt_prop IM selection A sender is tr.
-Proof.
+Proof using no_initial_messages_in_IM can_emit_signed Hsender_safety H6 H3.
   intro Htr.
   apply (VLSM_incl_finite_valid_trace fixed_non_equivocating_incl_fixed_non_byzantine).
   specialize
@@ -646,7 +647,7 @@ Lemma fixed_non_byzantine_vlsm_lift_valid
   : weak_embedding_valid_preservation PreNonByzantine Fixed
     (lift_sub_label IM (elements selection_complement))
     (lift_sub_state IM (elements selection_complement)).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm.
   intros l s om Hv HsY HomY.
   split.
   - by apply lift_sub_valid, Hv.
@@ -727,7 +728,7 @@ Lemma fixed_non_byzantine_vlsm_lift_from_initial
   : VLSM_embedding PreNonByzantine Fixed
       (lift_sub_label IM (elements selection_complement))
       (lift_sub_state IM (elements selection_complement)).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull Hfixed_non_byzantine_vlsm_lift_initial_message H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm.
   apply basic_VLSM_embedding.
   - by intro; intros; apply fixed_non_byzantine_vlsm_lift_valid.
   - by intro; intros * []; rapply lift_sub_transition.
@@ -737,7 +738,7 @@ Qed.
 
 Lemma fixed_non_byzantine_incl_fixed_non_equivocating_from_initial
   : VLSM_incl PreNonByzantine FixedNonEquivocating.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull Hfixed_non_byzantine_vlsm_lift_initial_message H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm.
   apply basic_VLSM_incl.
   - intro; intros.
     exists (lift_sub_state IM (elements selection_complement) s).
@@ -759,7 +760,7 @@ Qed.
 
 Lemma fixed_non_byzantine_eq_fixed_non_equivocating_from_initial
   : VLSM_eq PreNonByzantine FixedNonEquivocating.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull Hfixed_non_byzantine_vlsm_lift_initial_message H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm.
   apply VLSM_eq_incl_iff.
   split.
   - by apply fixed_non_byzantine_incl_fixed_non_equivocating_from_initial.
@@ -777,7 +778,7 @@ Context
 Lemma validator_fixed_non_byzantine_vlsm_lift_initial_message
   : weak_embedding_initial_message_preservation PreNonByzantine Fixed
     (lift_sub_state IM (elements selection_complement)).
-Proof.
+Proof using Hvalidator H6 H3.
   intros l s m Hv HsY HmX.
   destruct HmX as [[sub_i [[im Him] Heqm]] | Hseeded].
   - simpl in Heqm. subst.
@@ -800,7 +801,7 @@ Qed.
 *)
 Lemma validator_fixed_non_byzantine_eq_fixed_non_equivocating
   : VLSM_eq PreNonByzantine FixedNonEquivocating.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hvalidator Hsender_safety Hfull H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm.
   apply fixed_non_byzantine_eq_fixed_non_equivocating_from_initial.
   by apply validator_fixed_non_byzantine_vlsm_lift_initial_message.
 Qed.
@@ -824,7 +825,7 @@ Lemma validator_fixed_byzantine_traces_equivocation_char bis btr
       composite_state_sub_projection IM (elements selection_complement) bis /\
       finite_trace_sub_projection IM (elements selection_complement) etr =
       finite_trace_sub_projection IM (elements selection_complement) btr.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hvalidator Hsender_safety Hfull H6 H3 H18 H17 H16 H15 H14 H13 H12 H11 H10 EqDecision1 Cm.
   unfold fixed_byzantine_trace_alt_prop.
   split; intros Htr.
   - apply fixed_non_equivocating_traces_char.
diff --git a/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v b/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v
index b7abed9a..27789d0f 100644
--- a/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v
+++ b/theories/VLSM/Core/ByzantineTraces/LimitedByzantineTraces.v
@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From stdpp Require Import prelude finite.
 From Coq Require Import FunctionalExtensionality Reals.
 From VLSM.Lib Require Import Preamble FinSetExtras ListFinSetExtras.
@@ -108,7 +109,7 @@ Lemma limited_PreNonByzantine_valid_state_lift_not_heavy s
   (Hs : valid_state_prop PreNonByzantine s)
   (sX := lift_sub_state IM (elements non_byzantine) s)
   : tracewise_not_heavy sX.
-Proof.
+Proof using Inj0 Hlimit H6 H3.
   cut (tracewise_equivocating_validators sX ⊆ byzantine_vs).
   {
     intro Hincl.
@@ -177,7 +178,7 @@ Lemma limited_PreNonByzantine_lift_valid
   : weak_embedding_valid_preservation PreNonByzantine Limited
     (lift_sub_label IM (elements non_byzantine))
     (lift_sub_state IM (elements non_byzantine)).
-Proof.
+Proof using Inj0 Hlimit H6 H3.
   intros l s om Hv HsY HomY.
   repeat split; [by apply lift_sub_valid, Hv |].
   hnf.
@@ -200,7 +201,7 @@ Lemma limited_PreNonByzantine_vlsm_lift
   : VLSM_embedding PreNonByzantine Limited
       (lift_sub_label IM (elements non_byzantine))
       (lift_sub_state IM (elements non_byzantine)).
-Proof.
+Proof using Inj0 Hvalidator Hlimit H6 H3.
   apply basic_VLSM_embedding; intros ? *.
   - by intros; apply limited_PreNonByzantine_lift_valid.
   - by intros * []; rapply lift_sub_transition.
@@ -233,7 +234,7 @@ Lemma validator_fixed_limited_non_byzantine_traces_are_limited_non_equivocating
       composite_state_sub_projection IM (elements not_byzantine) bs /\
       finite_trace_sub_projection IM (elements not_byzantine) tr =
       finite_trace_sub_projection IM (elements not_byzantine) btr.
-Proof.
+Proof using Inj0 Hvalidator H6 H3.
   intros [Hlimit Hfixed].
   eexists _, _; split.
   - by apply (VLSM_embedding_finite_valid_trace
@@ -263,7 +264,7 @@ Lemma validator_limited_non_byzantine_traces_are_limited_non_equivocating s tr
         composite_state_sub_projection IM (elements selection_complement) bs /\
         finite_trace_sub_projection IM (elements selection_complement) tr =
         finite_trace_sub_projection IM (elements selection_complement) btr.
-Proof.
+Proof using Inj0 Hvalidator H6 H3.
   intros [byzantine Hlimited].
   apply proj1 in Hlimited as Hlimit.
   apply validator_fixed_limited_non_byzantine_traces_are_limited_non_equivocating
@@ -333,7 +334,7 @@ Lemma lift_pre_loaded_fixed_non_byzantine_valid_transition_to_limited
       (Build_annotated_state (free_composite_vlsm IM) Cv
         (lift_sub_state IM (elements non_byzantine) sub_sf) ann',
       oom).
-Proof.
+Proof using Hvalidator H17 H15 H14 EqDecision1.
   destruct sub_l as [sub_i li]; destruct_dec_sig sub_i i Hi Heqsub_i; subst.
   repeat split; cbn.
   - done.
@@ -389,7 +390,7 @@ Lemma lift_fixed_byzantine_traces_to_limited
         (finite_trace_sub_projection IM (elements non_byzantine) tr)))
   : finite_valid_trace Limited bs btr /\
     state_annotation (@finite_trace_last _ (type Limited) bs btr) ⊆ byzantine_vs.
-Proof.
+Proof using message_dependencies Inj0 Hvalidator Hfull H6 H3 H28 H27 H25 H24 H20 H17 H15 H14 FullMessageDependencies0 EqDecision2 EqDecision1.
   subst non_byzantine.
   induction Hbyzantine using finite_valid_trace_rev_ind; [repeat split |].
   - constructor; apply initial_state_is_valid.
@@ -474,7 +475,7 @@ Lemma msg_dep_validator_limited_non_equivocating_byzantine_traces_are_limited_no
         finite_trace_sub_projection IM (elements selection_complement)
           (pre_VLSM_embedding_finite_trace_project
             (type Limited) (composite_type IM) Datatypes.id original_state btr).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Inj0 Hvalidator Hfull Hchannel H6 H3 H28 H27 H25 H24 H20 H18 H17 H15 H14 FullMessageDependencies0 EqDecision2 EqDecision1.
   split.
   - intros (byzantine & Hlimited & Hbyzantine).
     apply lift_fixed_byzantine_traces_to_limited in Hbyzantine
diff --git a/theories/VLSM/Core/Composition.v b/theories/VLSM/Core/Composition.v
index 042f83f8..a7a9d4ea 100644
--- a/theories/VLSM/Core/Composition.v
+++ b/theories/VLSM/Core/Composition.v
@@ -4,6 +4,8 @@ From Coq Require Import Streams FunctionalExtensionality Eqdep_dec.
 From VLSM.Lib Require Import Preamble ListExtras.
 From VLSM.Core Require Import VLSM Plans VLSMProjections.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Composition
 
   This module provides Coq definitions for composite VLSMs and their projections
@@ -1105,7 +1107,7 @@ Context
 Lemma composite_decidable_initial_message
   (Hdec_init : forall i, vdecidable_initial_messages_prop (IM i))
   : decidable_initial_messages_prop (composite_vlsm_machine IM constraint).
-Proof.
+Proof using H.
   intro m. simpl. unfold composite_initial_message_prop.
   apply
     (Decision_iff
@@ -1411,39 +1413,39 @@ Context {message : Type}
 Lemma empty_composition_no_index
   (i : index)
   : False.
-Proof.
+Proof using Hempty_index H EqDecision0.
   by specialize (elem_of_enum i); rewrite Hempty_index; apply not_elem_of_nil.
 Qed.
 
 Lemma empty_composition_single_state
   (s : composite_state IM)
   : s = (proj1_sig (composite_s0 IM)).
-Proof.
+Proof using Hempty_index H EqDecision0.
   by extensionality i; elim (empty_composition_no_index i).
 Qed.
 
 Lemma empty_composition_no_label
   (l : composite_label IM)
   : False.
-Proof.
+Proof using Hempty_index H EqDecision0.
   by destruct l as [i _]; elim (empty_composition_no_index i).
 Qed.
 
 Lemma empty_composition_no_initial_message
   : forall m, ~ composite_initial_message_prop IM m.
-Proof.
+Proof using Hempty_index H EqDecision0.
   by intros m [i _]; elim (empty_composition_no_index i).
 Qed.
 
 Lemma empty_composition_no_emit
   : forall m, ~ can_emit X m.
-Proof.
+Proof using Hempty_index H.
   by intros m [s' [l _]]; elim (empty_composition_no_label l).
 Qed.
 
 Lemma empty_composition_no_valid_message
   : forall m, ~ valid_message_prop X m.
-Proof.
+Proof using Hempty_index H.
   intros m Hm.
   apply emitted_messages_are_valid_iff in Hm as [Hinit | Hemit].
   - by elim (empty_composition_no_initial_message _ Hinit).
@@ -1454,13 +1456,13 @@ Lemma pre_loaded_empty_composition_no_emit
   (seed : message -> Prop)
   (PreX := pre_loaded_vlsm X seed)
   : forall m, ~ can_emit PreX m.
-Proof.
+Proof using Hempty_index H.
   by intros m [s' [l _]]; elim (empty_composition_no_label l).
 Qed.
 
 Lemma pre_loaded_with_all_empty_composition_no_emit
   : forall m, ~ can_emit (pre_loaded_with_all_messages_vlsm X) m.
-Proof.
+Proof using Hempty_index H.
   by intros m [s' [l _]]; elim (empty_composition_no_label l).
 Qed.
 
@@ -1510,7 +1512,7 @@ Lemma same_IM_embedding
     (pre_loaded_vlsm (composite_vlsm IM2 constraint2) seed)
     same_IM_label_rew
     same_IM_state_rew.
-Proof.
+Proof using constraint_projection.
   apply basic_VLSM_embedding; intros l **.
   - destruct Hv as [Hs [Hom [Hv Hc]]].
     apply constraint_projection in Hc; cycle 1.
@@ -1666,7 +1668,7 @@ Context
 Lemma not_CompositeValidTransitionNext_initial :
   forall s2, composite_initial_state_prop IM s2 ->
   forall s1, ~ CompositeValidTransitionNext IM s1 s2.
-Proof.
+Proof using H.
   intros s2 Hs2 s1 [* Hs1].
   apply composite_valid_transition_projection, proj1, valid_transition_next in Hs1; cbn in Hs1.
   by contradict Hs1; apply not_ValidTransitionNext_initial, Hs2.
@@ -1678,7 +1680,7 @@ Lemma composite_quasi_unique_transition_to_state :
   forall [l2 s2 iom2 oom2], CompositeValidTransition IM l2 s2 iom2 s oom2 ->
   projT1 l1 = projT1 l2 ->
   l1 = l2 /\ s1 = s2 /\ iom1 = iom2 /\ oom1 = oom2.
-Proof.
+Proof using H.
   intros ? [i li1] * Ht1 [_i li2] * Ht2 [=]; subst _i.
   apply composite_valid_transition_projection in Ht1, Ht2; cbn in Ht1, Ht2.
   destruct Ht1 as [Ht1 Heq_s], Ht2 as [Ht2 Heqs].
@@ -1696,7 +1698,7 @@ Lemma CompositeValidTransition_reflects_rechability :
   CompositeValidTransition IM l s1 iom s2 oom ->
   valid_state_prop RFree s2 ->
   input_valid_transition RFree l (s1, iom) (s2, oom).
-Proof.
+Proof using H.
   intros * Hnext Hs2; revert l s1 iom oom Hnext.
   induction Hs2 using valid_state_prop_ind; intros * Hnext.
   - apply composite_valid_transition_next in Hnext.
@@ -1744,20 +1746,20 @@ Qed.
 Lemma CompositeValidTransitionNext_reflects_rechability :
   forall s1 s2, CompositeValidTransitionNext IM s1 s2 ->
     valid_state_prop RFree s2 -> valid_state_prop RFree s1.
-Proof.
+Proof using H.
   by intros s1 s2 []; eapply CompositeValidTransition_reflects_rechability.
 Qed.
 
 Lemma composite_valid_transition_future_reflects_rechability :
   forall s1 s2, composite_valid_transition_future IM s1 s2 ->
     valid_state_prop RFree s2 -> valid_state_prop RFree s1.
-Proof. by apply tc_reflect, CompositeValidTransitionNext_reflects_rechability. Qed.
+Proof using H. by apply tc_reflect, CompositeValidTransitionNext_reflects_rechability. Qed.
 
 Lemma composite_valid_transitions_from_to_reflects_reachability :
   forall s s' tr,
   CompositeValidTransitionsFromTo IM s s' tr ->
   valid_state_prop RFree s' -> finite_valid_trace_from_to RFree s s' tr.
-Proof.
+Proof using H.
   induction 1; intros; [by constructor |].
   assert (Hitem : input_valid_transition RFree (l item) (s', input item)
                           (destination item, output item))
diff --git a/theories/VLSM/Core/ELMO/BaseELMO.v b/theories/VLSM/Core/ELMO/BaseELMO.v
index 2cd77b5e..2e487627 100644
--- a/theories/VLSM/Core/ELMO/BaseELMO.v
+++ b/theories/VLSM/Core/ELMO/BaseELMO.v
@@ -1,9 +1,12 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude finite.
 From VLSM.Lib Require Import EquationsExtras.
 From VLSM.Lib Require Import Preamble StdppExtras.
 From VLSM.Core Require Import VLSM MessageDependencies.
 
+Set Default Proof Using "Type".
+
 (** * Basic Definitions and Lemmas for UMO, MO and ELMO
 
   This module contains basic definitions and lemmas needed for the UMO, MO and
@@ -77,7 +80,7 @@ Proof. by intros x y; unfold Decision; decide equality. Defined.
 #[local] Lemma State_eq_dec : forall x y : State, {x = y} + {x <> y}
 with Observation_eq_dec : forall x y : Observation, {x = y} + {x <> y}
 with Message_eq_dec : forall x y : Message, {x = y} + {x <> y}.
-Proof.
+Proof using EqDecision0.
   - intros x y; decide equality.
     + by apply EqDecision0.
     + by decide equality.
@@ -696,7 +699,7 @@ Definition ELMO_A (a : Address) : index :=
   hd inhabitant (filter (fun i => idx i = a) (enum index)).
 
 Lemma ELMO_A_inv : forall i, ELMO_A (idx i) = i.
-Proof.
+Proof using Inj0.
   intro i; unfold ELMO_A; cbn.
   replace (filter _ _) with [i]; [done |].
   generalize (enum index), (NoDup_enum index) as Hnodup, (elem_of_enum i) as Hi.
diff --git a/theories/VLSM/Core/ELMO/ELMO.v b/theories/VLSM/Core/ELMO/ELMO.v
index 31549ac8..68ca3d3b 100644
--- a/theories/VLSM/Core/ELMO/ELMO.v
+++ b/theories/VLSM/Core/ELMO/ELMO.v
@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From Coq Require Import FunctionalExtensionality Reals.
 From stdpp Require Import prelude finite.
@@ -7,6 +8,8 @@ From VLSM.Core Require Import Validator ProjectionTraces MessageDependencies.
 From VLSM.Core Require Import TraceableVLSM MinimalEquivocationTrace.
 From VLSM.Core Require Import BaseELMO UMO MO.
 
+Set Default Proof Using "Type".
+
 Create HintDb ELMO_hints.
 
 #[local] Hint Resolve submseteq_tail_l : ELMO_hints.
@@ -204,7 +207,7 @@ Proof.
 Qed.
 
 #[export] Instance local_equivocators_full_obs_dec : RelDecision local_equivocators_full_obs.
-Proof.
+Proof using EqDecision0.
   intros ol a.
   induction ol using addObservation'_rec.
   - by right; inversion 1.
@@ -326,7 +329,7 @@ Definition ELMOComponent (i : index) : VLSM Message :=
 
 #[export] Instance ComputableSentMessages_ELMOComponent
   (i : index) : ComputableSentMessages (ELMOComponent i).
-Proof.
+Proof using Inj0.
   constructor 1 with sentMessages; constructor.
   - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil.
   - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
@@ -340,7 +343,7 @@ Defined.
 
 #[export] Instance ComputableReceivedMessages_ELMOComponent
   (i : index) : ComputableReceivedMessages (ELMOComponent i).
-Proof.
+Proof using Inj0.
   constructor 1 with receivedMessages; constructor.
   - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil.
   - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
@@ -588,7 +591,7 @@ Lemma local_equivocators_simple_addObservation :
       adr (state (message ob)) = a /\
       message ob ∉ messages s /\
       exists m, m ∈ messages s /\ incomparable (message ob) m.
-Proof.
+Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca.
   intros s ob a [].
   apply elem_of_messages_addObservation in les_obs_m1 as [-> | Hm1], les_obs_m2 as [-> | Hm2].
   - by destruct les_incomparable as [? []]; constructor.
@@ -606,7 +609,7 @@ Lemma local_equivocators_simple_add_Send (s : State) :
   UMO_reachable no_self_equiv s ->
   forall a, local_equivocators_simple (s <+> MkObservation Send (MkMessage s)) a ->
             local_equivocators_simple s a.
-Proof.
+Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca.
   intros Hs a Ha.
   apply local_equivocators_simple_addObservation
     in Ha as [| (<- & _ & m & Hm & Hincomp)]; [done |]; cbn in *.
@@ -621,7 +624,7 @@ Qed.
 Lemma local_equivocators_simple_no_self (s : State) :
   UMO_reachable no_self_equiv s ->
     ~ local_equivocators_simple s (adr s).
-Proof.
+Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca.
   intros Hs; induction Hs as [| | ? ? Hno_self_eqv].
   - by destruct 1; inversion les_obs_m1.
   - by contradict IHHs; apply local_equivocators_simple_add_Send in IHHs.
@@ -665,7 +668,7 @@ Lemma local_equivocators_simple_add_Receive (s : State) (msg : Message) :
             local_equivocators_simple s i
      \/ adr (state msg) = i /\ i <> adr s /\
           exists m, m ∈ messages s /\ incomparable msg m.
-Proof.
+Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca.
   intros Hs Hno_equiv a Ha.
   assert (a <> adr (s <+> MkObservation Receive msg))
     by (contradict Ha; subst; apply local_equivocators_simple_no_self; constructor; done).
@@ -743,7 +746,7 @@ Qed.
 Lemma local_equivocators_simple_iff_full (s : State) :
   UMO_reachable no_self_equiv s ->
   forall a, local_equivocators_simple s a <-> local_equivocators_full s a.
-Proof.
+Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca.
   intros Hs a; split.
   - induction Hs.
     + by destruct 1; inversion les_obs_m1.
@@ -782,7 +785,7 @@ Qed.
 Lemma local_equivocators_iff_full (s : State) :
   UMO_reachable (fun s m => full_node s m /\ no_self_equiv s m) s ->
   forall a, local_equivocators s a <-> local_equivocators_full s a.
-Proof.
+Proof using threshold measurable_Address index idx i Ri ReachableThreshold0 H7 H6 H5 H4 H3 H2 H1 H0 H EqDecision1 EqDecision0 Ei Ca.
   intros Hs a.
   by rewrite local_equivocators_iff_simple;
     [apply local_equivocators_simple_iff_full |];
@@ -871,7 +874,7 @@ Lemma equivocation_limit_recv_ok_msg_ok (s : State) (m : Message) :
   UMO_reachable no_self_equiv (state m) ->
   local_equivocation_limit_ok (s <+> MkObservation Receive m) ->
   local_equivocation_limit_ok (state m).
-Proof.
+Proof using i Ri Ei.
   intros Hfull Hno_self Hs Hms Hs'.
   eapply Rle_trans; [| done].
   apply incl_equivocating_validators_equivocation_fault, filter_subprop; cbn; intros a Ha.
@@ -998,7 +1001,7 @@ Lemma reachable_received_messages_reachable (s : State) :
   forall i',
     adr (state m) = idx i' ->
     ram_state_prop (ELMOComponent i') (state m).
-Proof.
+Proof using Inj0.
   intros Hs m Hm.
   destruct (decide (adr (state m) = adr s)).
   {
@@ -1067,7 +1070,7 @@ Lemma receivable_messages_reachable (ms s : State) i' :
   ram_state_prop Ei s ->
   ELMO_recv_valid s (MkMessage ms) ->
   ram_state_prop (ELMOComponent i') ms.
-Proof.
+Proof using Inj0.
   intros Heq Hram Hrv.
   change ms with (state (MkMessage ms)).
   apply reachable_received_messages_reachable
@@ -1119,7 +1122,7 @@ Lemma ELMOComponent_receivedMessages_of_ram_trace
   [s s' tr] (Htr : finite_valid_trace_from_to Ri s s' tr) :
   forall item, item ∈ tr ->
   forall m, (field_selector input) m item -> m ∈ receivedMessages s'.
-Proof.
+Proof using Inj0.
   induction Htr using finite_valid_trace_from_to_rev_ind; [by inversion 1 |].
   intros item Hitem m Hm.
   change (has_been_received Ei sf m).
@@ -1132,7 +1135,7 @@ Lemma ELMOComponent_sentMessages_of_ram_trace
   [s s' tr] (Htr : finite_valid_trace_from_to Ri s s' tr) :
   forall item, item ∈ tr ->
   forall m, (field_selector output) m item -> m ∈ sentMessages s'.
-Proof.
+Proof using Inj0.
   induction Htr using finite_valid_trace_from_to_rev_ind; [by inversion 1 |].
   intros item Hitem m Hm.
   change (has_been_sent Ei sf m).
@@ -1158,7 +1161,7 @@ Lemma ELMOComponent_messages_of_ram_trace
   [s s' tr] (Htr : finite_valid_trace_from_to Ri s s' tr) :
   forall item, item ∈ tr ->
   forall m, item_sends_or_receives m item -> m ∈ messages s'.
-Proof.
+Proof using Inj0.
   intros ? ? ? [|]; apply elem_of_messages.
   - by right; eapply ELMOComponent_receivedMessages_of_ram_trace.
   - by left; eapply ELMOComponent_sentMessages_of_ram_trace.
@@ -1552,7 +1555,7 @@ Qed.
 
 Lemma ELMO_channel_authentication_prop :
   channel_authentication_prop ELMOComponent (ELMO_A idx) Message_sender.
-Proof.
+Proof using Inj0.
   intros i m ((s, []) & [] & s' & [(Hs & _ & Hv) Ht]);
     inversion Hv; subst; inversion Ht; subst.
   unfold channel_authenticated_message; cbn; f_equal.
@@ -2003,7 +2006,7 @@ Lemma ELMO_update_state_with_initial
     ELMO_equivocating_validators (state_update ELMOComponent s i si)
       ⊆
     ELMO_equivocating_validators s ∪ {[ idx i ]}.
-Proof.
+Proof using H8.
   assert (Hincl : VLSM_incl ELMOProtocol ReachELMO) by apply constraint_preloaded_free_incl.
   assert (Htr_min := ELMO_state_to_minimal_equivocation_trace_valid _ Hs).
   cbn in Htr_min; destruct (ELMO_state_to_minimal_equivocation_trace _ _)
@@ -2110,7 +2113,7 @@ Lemma ELMO_valid_states_only_receive_valid_messages :
   forall (i : index) (l : Label) (s' : vstate ELMOProtocol) (m : Message),
     ELMOProtocolValidTransition i l s s' m ->
     valid_message_prop ELMOProtocol m.
-Proof.
+Proof using H8.
   intros s Hs i l s' m Hvalid.
   inversion Hvalid as [? ? ? ? Hreceive | ? ? ? ? Hsend]; subst; cycle 1.
   {
@@ -2815,7 +2818,7 @@ Lemma reflecting_composite_for_reachable_component
       let s' := state_update ELMOComponent s i s_prev in
       valid_state_prop ELMOProtocol s' /\
       ELMOProtocolValidTransition i l s' s m.
-Proof.
+Proof using H8.
   induction Hreachable using valid_state_prop_ind;
     [| destruct IHHreachable as (sigma & <- & Hsigma & Hreflects & Hsend & Hall), l; cycle 1].
   - unfold initial_state_prop in Hs; cbn in Hs.
@@ -3011,7 +3014,7 @@ Qed.
 Theorem ELMOComponents_validating :
   forall i : index,
     component_projection_validator_prop ELMOComponent ELMO_global_constraint i.
-Proof.
+Proof using H8.
   intros i li si om Hvti.
   apply input_valid_transition_iff in Hvti as [[si' om'] Hvti].
   pose (Hvti' := Hvti); destruct Hvti' as [(_ & _ & Hvi) Hti].
diff --git a/theories/VLSM/Core/ELMO/MO.v b/theories/VLSM/Core/ELMO/MO.v
index d4fcba8a..2f310085 100644
--- a/theories/VLSM/Core/ELMO/MO.v
+++ b/theories/VLSM/Core/ELMO/MO.v
@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From Coq Require Import FunctionalExtensionality.
 From stdpp Require Import prelude finite.
@@ -713,7 +714,7 @@ Lemma state_suffix_totally_orders_valid_sent_messages :
       obs1 <*> MkObservation Send m1 <**> obs2 <*> MkObservation Send m2 <**> obs3 ->
     MO_msg_valid_alt_sends m ->
       state_suffix (state m1) (state m2) /\ state_suffix (state m2) (state m).
-Proof.
+Proof using P.
   intros m m1 m2 obs1 obs2 obs3 Heq Hvalid.
   red in Hvalid.
   assert (H2 :
@@ -1228,7 +1229,7 @@ Lemma unfold_rec_obs :
     rec_obs s ob
       <->
     ob ∈ obs s \/ exists m, MkObservation Receive m ∈ obs s /\ rec_obs (state m) ob.
-Proof using. clear. (* avoid unneccessary dependence on section variables *)
+Proof. clear -Message. (* avoid unneccessary dependence on section variables *)
   intros s ob; split.
   - induction 1.
     + by left; constructor.
diff --git a/theories/VLSM/Core/ELMO/UMO.v b/theories/VLSM/Core/ELMO/UMO.v
index 481a06ad..52331dc6 100644
--- a/theories/VLSM/Core/ELMO/UMO.v
+++ b/theories/VLSM/Core/ELMO/UMO.v
@@ -5,6 +5,8 @@ From VLSM.Lib Require Import Preamble StdppExtras StdppListSet.
 From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation ProjectionTraces.
 From VLSM.Core Require Import BaseELMO.
 
+Set Default Proof Using "Type".
+
 (** * UMO Protocol Definitions and Properties
 
   This module contains definitions and properties of UMO components and
@@ -105,7 +107,7 @@ Qed.
 
 #[export] Instance HasBeenSentCapability_UMOComponent
   (i : Address) : HasBeenSentCapability (UMOComponent i).
-Proof.
+Proof using EqDecision0.
   apply Build_HasBeenSentCapability with (fun s m => m ∈ sentMessages s)
   ; [by intros s m; typeclasses eauto |].
   split.
@@ -121,7 +123,7 @@ Defined.
 
 #[export] Instance HasBeenReceivedCapability_UMOComponent
   (i : Address) : HasBeenReceivedCapability (UMOComponent i).
-Proof.
+Proof using EqDecision0.
   eapply Build_HasBeenReceivedCapability with (fun s m => m ∈ receivedMessages s)
   ; [intros s m; typeclasses eauto | split].
   - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil.
@@ -1399,7 +1401,7 @@ End sec_UMOComponent_lemmas.
 Proof. by intros x y []; constructor. Defined.
 
 #[export] Instance sent_comparable_dec : RelDecision sent_comparable.
-Proof.
+Proof using EqDecision0.
   intros m1 m2.
   destruct (decide (adr (state m1) = adr (state m2)));
     [| by right; destruct 1; apply n; firstorder congruence].
@@ -1599,7 +1601,7 @@ Lemma finite_valid_trace_from_to_UMO_state2trace_UMO :
   forall us : UMO_state,
     valid_state_prop UMO us ->
       finite_valid_trace_init_to UMO (``(vs0 UMO)) us (UMO_state2trace us).
-Proof.
+Proof using EqDecision0.
   intros us Hvsp.
   apply all_pre_traces_to_valid_state_are_valid; [typeclasses eauto | done |].
   apply finite_valid_trace_from_to_UMO_state2trace_RUMO.
@@ -1661,7 +1663,7 @@ Lemma elem_of_UMO_sentMessages :
   forall (us : UMO_state) (m : Message) (i : index),
     valid_state_prop RUMO us -> idx i = adr (state m) ->
       m ∈ UMO_sentMessages us <-> m ∈ sentMessages (us i).
-Proof.
+Proof using Inj0.
   intros us m i Hvsp Hidx.
   assert (Hall : forall i, i ∉ enum index -> us i = MkState [] (idx i))
     by (intros j Hin; contradict Hin; apply elem_of_enum).
@@ -1704,7 +1706,7 @@ Lemma UMO_sentMessages_characterization :
         <->
       let s' := state m <+> MkObservation Send m in
         state_suffix s' (us i) \/ s' = us i.
-Proof.
+Proof using Inj0.
   intros us m i Hvsp Hidx.
   rewrite elem_of_UMO_sentMessages by done.
   rewrite <- sentMessages_characterization; [done |].
diff --git a/theories/VLSM/Core/Equivocation.v b/theories/VLSM/Core/Equivocation.v
index d30eb58e..291d55f5 100644
--- a/theories/VLSM/Core/Equivocation.v
+++ b/theories/VLSM/Core/Equivocation.v
@@ -6,6 +6,8 @@ From VLSM.Lib Require Import ListSetExtras Measurable.
 From VLSM.Core Require Import VLSM VLSMProjections Composition ProjectionTraces Validator.
 From VLSM.Core Require Export ReachableThreshold.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocation Definitions
 
   This module is dedicated to building the vocabulary for discussing equivocation.
@@ -881,7 +883,7 @@ Lemma prove_all_have_message_from_stepwise :
          (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s)
          (m : message),
     all_traces_have_message_prop vlsm selector oracle s m.
-Proof.
+Proof using oracle_props.
   intros s Hproto m.
   unfold all_traces_have_message_prop.
   split.
@@ -898,7 +900,7 @@ Lemma prove_none_have_message_from_stepwise :
          (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s)
          (m : message),
     no_traces_have_message_prop vlsm selector (fun s m => ~ oracle s m) s m.
-Proof.
+Proof using oracle_props.
   intros s Hproto m.
   split.
   - intros H_not_holds start tr Htr.
@@ -916,7 +918,7 @@ Lemma selected_messages_consistency_prop_from_stepwise
     (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s)
     (m : message)
     : selected_messages_consistency_prop vlsm selector s m.
-Proof.
+Proof using oracle_props.
   split; [| by apply consistency_from_valid_state_proj2].
   intro Hsome.
   destruct (decide (oracle s m)) as [Hsm | Hsm].
@@ -931,7 +933,7 @@ Lemma in_futures_preserving_oracle_from_stepwise :
     (Hfutures : in_futures (pre_loaded_with_all_messages_vlsm vlsm) s1 s2)
     (m : message),
     oracle s1 m -> oracle  s2 m.
-Proof.
+Proof using selector oracle_props.
   intros s1 s2 [tr Htr] m Hs1m.
   by eapply oracle_partial_trace_update; [| | right].
 Qed.
@@ -963,7 +965,7 @@ Context
 Lemma oracle_no_inits_from_trace :
   forall (s : vstate vlsm), initial_state_prop (VLSMMachine := vmachine vlsm) s ->
                            forall m, ~ oracle s m.
-Proof.
+Proof using selector Horacle_all_have.
   intros s Hinit m Horacle.
   assert (Hproto : valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s)
     by (apply initial_state_is_valid; done).
@@ -979,7 +981,7 @@ Lemma examine_one_trace :
   forall m,
     oracle s m <->
     trace_has_message selector m tr.
-Proof.
+Proof using oracle_dec Horacle_all_have Hnot_oracle_none_have.
   intros is s tr Htr m.
   assert (valid_state_prop (pre_loaded_with_all_messages_vlsm vlsm) s)
     by (apply valid_trace_last_pstate in Htr; done).
@@ -1002,7 +1004,7 @@ Lemma oracle_step_property_from_trace :
        forall msg, oracle s' msg
                    <-> (selector msg {| l := l; input := im; destination := s'; output := om |}
                         \/ oracle s msg).
-Proof.
+Proof using oracle_dec Horacle_all_have Hnot_oracle_none_have.
   intros l s im s' om Htrans msg.
   rename Htrans into Htrans'.
   pose proof Htrans' as [[Hproto_s [Hproto_m Hvalid]] Htrans].
@@ -1019,7 +1021,7 @@ Proof.
 Qed.
 
 Lemma stepwise_props_from_trace : oracle_stepwise_props selector oracle.
-Proof.
+Proof using oracle_dec Horacle_all_have Hnot_oracle_none_have.
   constructor.
   - by apply oracle_no_inits_from_trace.
   - by apply oracle_step_property_from_trace.
@@ -1493,7 +1495,7 @@ Qed.
 
 Lemma com_computable_oracle :
   computable_messages_oracle vlsm directly_observed_messages_set item_sends_or_receives.
-Proof.
+Proof using EqDecision0.
   constructor; intros.
   - setoid_rewrite directly_observed_messages_set_iff.
     + by apply has_been_directly_observed_stepwise_props.
@@ -1633,7 +1635,7 @@ Context
   .
 
 Definition composite_message_selector : message -> composite_transition_item IM -> Prop.
-Proof.
+Proof using message_selectors.
   intros msg [[i li] input s output].
   apply (message_selectors i msg).
   exact {| l := li; input := input; destination := s i; output := output |}.
@@ -1646,7 +1648,7 @@ Lemma composite_stepwise_props
   (constraint : composite_label IM -> composite_state IM * option message -> Prop)
   (X := composite_vlsm IM constraint)
   : oracle_stepwise_props (vlsm := X) composite_message_selector composite_oracle.
-Proof.
+Proof using stepwise_props.
   split.
   - (* initial states not claim *)
     intros s Hs m [i Horacle].
@@ -1693,7 +1695,7 @@ Lemma oracle_component_selected_previously
     in_futures X (destination item) s /\
     projT1 (l item) = i /\
     composite_message_selector m item.
-Proof.
+Proof using stepwise_props.
   apply valid_state_has_trace in Hs as (is & tr & Htr).
   eapply VLSM_incl_finite_valid_trace_init_to in Htr as Hpre_tr
   ; [| by apply constraint_preloaded_free_incl].
@@ -1735,7 +1737,7 @@ Definition composite_has_been_sent
 
 (** [composite_has_been_sent] is decidable. *)
 Lemma composite_has_been_sent_dec : RelDecision composite_has_been_sent.
-Proof.
+Proof using H EqDecision0.
   intros s m.
   apply (Decision_iff (P := List.Exists (fun i => has_been_sent (IM i) (s i) m) (enum index))).
   - by rewrite Exists_finite.
@@ -1768,7 +1770,7 @@ Lemma composite_proper_sent
   (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)) s)
   (m : message)
   : has_been_sent_prop (free_composite_vlsm IM) composite_has_been_sent s m.
-Proof.
+Proof using H.
   specialize (proper_sent (free_composite_vlsm IM)) as Hproper_sent.
   by apply Hproper_sent.
 Qed.
@@ -1787,7 +1789,7 @@ Definition composite_has_been_received
 
 (** [composite_has_been_received] is decidable. *)
 Lemma composite_has_been_received_dec : RelDecision composite_has_been_received.
-Proof.
+Proof using H EqDecision0.
   intros s m.
   apply (Decision_iff (P := List.Exists (fun i => has_been_received (IM i) (s i) m) (enum index))).
   - by rewrite Exists_finite.
@@ -1858,7 +1860,7 @@ Definition composite_has_been_directly_observed
 
 (** [composite_has_been_directly_observed] is decidable. *)
 Lemma composite_has_been_directly_observed_dec : RelDecision composite_has_been_directly_observed.
-Proof.
+Proof using H EqDecision0.
   intros s m.
   apply (Decision_iff
     (P := List.Exists (fun i => has_been_directly_observed (IM i) (s i) m) (enum index))).
@@ -1882,7 +1884,7 @@ Definition composite_HasBeenDirectlyObservedCapability_from_stepwise
   (constraint : composite_label IM -> composite_state IM * option message -> Prop)
   (X := composite_vlsm IM constraint)
   : HasBeenDirectlyObservedCapability X.
-Proof.
+Proof using H1 H0 H.
   exists composite_has_been_directly_observed.
   - by apply composite_has_been_directly_observed_dec.
   - by apply (composite_has_been_directly_observed_stepwise_props constraint).
@@ -1938,7 +1940,7 @@ Definition sender_safety_alt_prop : Prop :=
 
 Lemma sender_safety_alt_iff
   : sender_safety_prop <-> sender_safety_alt_prop.
-Proof.
+Proof using EqDecision0.
   split; intros Hsender_safety m; intros.
   - specialize (Hsender_safety m v Hsender).
     destruct (decide (i = A v)); [done |].
@@ -2149,7 +2151,6 @@ Lemma sent_component_sent_previously
     projT1 (l item) = i /\
     output item = Some m.
 Proof.
-  clear -Hs Horacle.
   specialize
     (oracle_component_selected_previously
       (fun i => has_been_sent_stepwise_props (IM i))
@@ -2172,7 +2173,6 @@ Lemma received_component_received_previously
     projT1 (l item) = i /\
     input item = Some m.
 Proof.
-  clear -Hs Horacle.
   specialize
     (oracle_component_selected_previously
       (fun i => has_been_received_stepwise_props (IM i))
@@ -2213,7 +2213,7 @@ Lemma messages_sent_from_component_of_valid_state_are_valid
   (m : message)
   (Hsent : has_been_sent (IM i) (s i) m) :
   valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H0 IM index message.
   by apply (sent_valid X s); [| exists i].
 Qed.
 
@@ -2227,7 +2227,7 @@ Lemma preloaded_messages_sent_from_component_of_valid_state_are_valid
   (m : message)
   (Hsent : has_been_sent (IM i) (s i) m) :
   valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H0 IM index message.
   by eapply sent_valid; [| exists i].
 Qed.
 
@@ -2240,7 +2240,7 @@ Lemma messages_received_from_component_of_valid_state_are_valid
   (m : message)
   (Hreceived : has_been_received (IM i) (s i) m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H1 IM index message.
   by eapply received_valid; [| exists i].
 Qed.
 
@@ -2254,7 +2254,7 @@ Lemma preloaded_messages_received_from_component_of_valid_state_are_valid
   (m : message)
   (Hreceived : has_been_received (IM i) (s i) m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H1 IM index message.
   by eapply received_valid; [| exists i].
 Qed.
 
@@ -2266,7 +2266,7 @@ Lemma composite_sent_valid
   (m : message)
   (Hsent : composite_has_been_sent s m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H0 IM index message.
   destruct Hsent as [i Hsent].
   by apply messages_sent_from_component_of_valid_state_are_valid with s i.
 Qed.
@@ -2280,7 +2280,7 @@ Lemma preloaded_composite_sent_valid
   (m : message)
   (Hsent : composite_has_been_sent s m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H0 IM index message.
   destruct Hsent as [i Hsent].
   by apply preloaded_messages_sent_from_component_of_valid_state_are_valid with s i.
 Qed.
@@ -2293,7 +2293,7 @@ Lemma composite_received_valid
   (m : message)
   (Hreceived : composite_has_been_received s m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H1 IM index message.
   destruct Hreceived as [i Hreceived].
   by apply messages_received_from_component_of_valid_state_are_valid with s i.
 Qed.
@@ -2307,7 +2307,7 @@ Lemma preloaded_composite_received_valid
   (m : message)
   (Hreceived : composite_has_been_received s m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H1 IM index message.
   destruct Hreceived as [i Hreceived].
   by apply preloaded_messages_received_from_component_of_valid_state_are_valid with s i.
 Qed.
@@ -2320,7 +2320,7 @@ Lemma composite_directly_observed_valid
   (m : message)
   (Hobserved : composite_has_been_directly_observed s m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H0 H1 IM index message.
   destruct Hobserved as [i Hobserved].
   apply (has_been_directly_observed_sent_received_iff (IM i)) in Hobserved.
   - destruct Hobserved as [Hreceived | Hsent].
@@ -2338,7 +2338,7 @@ Lemma preloaded_composite_directly_observed_valid
   (m : message)
   (Hobserved : composite_has_been_directly_observed s m)
   : valid_message_prop X m.
-Proof.
+Proof using EqDecision0 Free H H0 H1 IM index message.
   destruct Hobserved as [i Hobserved].
   apply (has_been_directly_observed_sent_received_iff (IM i)) in Hobserved.
   - destruct Hobserved as [Hreceived | Hsent].
@@ -2632,7 +2632,7 @@ Context
 Lemma input_valid_transition_received_not_resent l s m s' om'
   (Ht : input_valid_transition (pre_loaded_with_all_messages_vlsm X) l (s, Some m) (s', om'))
   : om' <> Some m.
-Proof.
+Proof using H H0 Hno_resend X message.
   destruct om' as [m' |]; [| by congruence].
   intro Heq. inversion Heq. subst m'. clear Heq.
   destruct (Hno_resend _ _ _ _ _ Ht) as [_ Hnbr_m].
@@ -2653,7 +2653,7 @@ Lemma lift_preloaded_trace_to_seeded
   (is : state)
   (Htr : finite_valid_trace PreX is tr)
   : finite_valid_trace (pre_loaded_vlsm X P) is tr.
-Proof.
+Proof using EqDecision0 H H0 Hno_resend PreX X message.
   unfold trace_received_not_sent_before_or_after_invariant in Htrm.
   split; [| by apply Htr].
   induction Htr using finite_valid_trace_rev_ind; intros.
@@ -2707,7 +2707,7 @@ Lemma lift_preloaded_state_to_seeded
   (Hequiv_s : state_received_not_sent_invariant s P)
   (Hs : valid_state_prop PreX s)
   : valid_state_prop (pre_loaded_vlsm X P) s.
-Proof.
+Proof using EqDecision0 H H0 Hno_resend PreX X message.
   apply valid_state_has_trace in Hs as Htr.
   destruct Htr as [is [tr Htr]].
   specialize (lift_preloaded_trace_to_seeded P tr) as Hlift.
@@ -2725,7 +2725,7 @@ Lemma lift_generated_to_seeded
   (m : message)
   (Hgen : can_produce PreX s m)
   : can_produce (pre_loaded_vlsm X P) s m.
-Proof.
+Proof using EqDecision0 H H0 Hno_resend PreX X message.
   apply non_empty_valid_trace_from_can_produce.
   apply non_empty_valid_trace_from_can_produce in Hgen.
   destruct Hgen as [is [tr [item [Htr Hgen]]]].
@@ -2798,7 +2798,7 @@ Lemma all_pre_traces_to_valid_state_are_valid
   is tr
   (Htr : finite_valid_trace_init_to PreX is s tr)
   : finite_valid_trace_init_to X is s tr.
-Proof.
+Proof using EqDecision0 H H0 IM PreX X constraint index message.
   apply pre_traces_with_valid_inputs_are_valid in Htr; [done |].
   apply valid_trace_last_pstate in Htr as Hspre.
   intros.
diff --git a/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v b/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v
index 4f5abd30..8cc5b9df 100644
--- a/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/FixedSetEquivocation.v
@@ -5,6 +5,8 @@ From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM VLSMProjections Composition Validator ProjectionTraces.
 From VLSM.Core Require Import SubProjectionTraces Equivocation Equivocation.NoEquivocation.
 
+Set Default Proof Using "Type".
+
 (** * Fixed Set Equivocation
 
   In this section we define fixed equivocation for the regular composition.
@@ -115,7 +117,7 @@ Definition sent_by_non_equivocating s m
   := exists i, i ∉ elements equivocating /\ has_been_sent (IM i) (s i) m.
 
 #[export] Instance sent_by_non_equivocating_dec : RelDecision sent_by_non_equivocating.
-Proof.
+Proof using H7 EqDecision0.
   intros s m.
   apply @Decision_iff with (P := Exists (fun i => has_been_sent (IM i) (s i) m)
     (filter (fun i => i ∉ elements equivocating) (enum index))).
@@ -136,7 +138,7 @@ Qed.
 Lemma sent_by_non_equivocating_are_directly_observed s m
   (Hsent : sent_by_non_equivocating s m)
   : composite_has_been_directly_observed IM s m.
-Proof.
+Proof using EqDecision0.
   apply composite_has_been_directly_observed_sent_received_iff; left.
   by apply sent_by_non_equivocating_are_sent.
 Qed.
@@ -241,7 +243,7 @@ Lemma fixed_equivocation_index_incl_subsumption
   : forall s m,
     fixed_equivocation IM indices1 s m ->
     fixed_equivocation IM indices2 s m.
-Proof.
+Proof using Hincl.
   intros s m [Hobs | Hemit]; [by left |].
   right.
   specialize
@@ -254,7 +256,7 @@ Lemma fixed_equivocation_constraint_index_incl_subsumption
   : strong_constraint_subsumption IM
     (fixed_equivocation_constraint IM indices1)
     (fixed_equivocation_constraint IM indices2).
-Proof.
+Proof using Hincl.
   intros l (s, [m |]); [| done].
   by apply fixed_equivocation_index_incl_subsumption.
 Qed.
@@ -263,7 +265,7 @@ Lemma fixed_equivocation_vlsm_composition_index_incl
   : VLSM_incl
     (fixed_equivocation_vlsm_composition IM indices1)
     (fixed_equivocation_vlsm_composition IM indices2).
-Proof.
+Proof using Hincl.
   apply constraint_subsumption_incl.
   apply preloaded_constraint_subsumption_stronger.
   apply strong_constraint_subsumption_strongest.
@@ -399,7 +401,7 @@ Context
   l m
   (Hv : input_valid Fixed l (s, Some m))
   : strong_fixed_equivocation IM equivocators base_s m.
-Proof.
+Proof using Hobs_s_protocol.
   destruct Hv as [_ [_ [_ [Hobs | Hemit]]]].
   - by apply Hobs_s_protocol.
   - right.
@@ -424,7 +426,7 @@ Qed.
       (composite_label_sub_projection IM (elements equivocators) l e)
       (composite_state_sub_projection IM (elements equivocators) s, iom)
       (composite_state_sub_projection IM (elements equivocators) sf, oom).
-Proof.
+Proof using Hobs_s_protocol.
   destruct l as (i, li). simpl in *.
   repeat split.
   - done.
@@ -453,7 +455,7 @@ Qed.
   l iom om
   (Ht : input_valid_transition Fixed l (s, iom) (sf, Some om))
   : strong_fixed_equivocation IM equivocators base_s om.
-Proof.
+Proof using Hobs_s_protocol.
   destruct (decide (projT1 l ∈ elements equivocators)).
   - apply
       (fixed_input_valid_transition_sub_projection_helper Hs_pr _ e) in Ht.
@@ -495,7 +497,7 @@ Lemma fixed_finite_valid_trace_sub_projection_helper
     (finite_trace_sub_projection IM (elements equivocators) tr) /\
     forall m, composite_has_been_directly_observed IM s m ->
       strong_fixed_equivocation IM equivocators base_s m.
-Proof.
+Proof using H7.
   induction Htr using finite_valid_trace_init_to_rev_ind.
   - split.
     + apply finite_valid_trace_from_to_empty.
@@ -559,7 +561,7 @@ Lemma fixed_finite_valid_trace_sub_projection is f tr
               (composite_state_sub_projection IM (elements equivocators) is)
               (composite_state_sub_projection IM (elements equivocators) f)
               (finite_trace_sub_projection IM (elements equivocators) tr).
-Proof.
+Proof using H7.
   apply fixed_finite_valid_trace_sub_projection_helper with (base_s := f) in Htr as Htr_pr.
   - split; [by apply Htr_pr |].
     apply proj2 in Htr.
@@ -578,7 +580,7 @@ Lemma fixed_directly_observed_has_strong_fixed_equivocation f
   m
   (Hobs : composite_has_been_directly_observed IM f m)
   : strong_fixed_equivocation IM equivocators f m.
-Proof.
+Proof using H7.
   apply (VLSM_incl_valid_state Fixed_incl_Preloaded) in Hf as Hfuture.
   apply in_futures_refl in Hfuture.
   apply valid_state_has_trace in Hf as [is [tr Htr]].
@@ -591,7 +593,7 @@ Lemma fixed_valid_state_sub_projection s f
   : valid_state_prop
     (equivocators_composition_for_sent IM equivocators f)
     (composite_state_sub_projection IM (elements equivocators) s).
-Proof.
+Proof using H7.
   destruct Hsf as [tr Htr].
   apply finite_valid_trace_from_to_complete_left in Htr as [is [trs [Htr Hs]]].
   apply fixed_finite_valid_trace_sub_projection in Htr as Hpr_tr.
@@ -610,7 +612,7 @@ Lemma fixed_input_has_strong_fixed_equivocation
   l s m
   (Ht : input_valid Fixed l (s, Some m))
   : strong_fixed_equivocation IM equivocators s m.
-Proof.
+Proof using H7.
   apply fixed_input_has_strong_fixed_equivocation_helper with (base_s := s) in Ht
   ; [done |].
   by apply fixed_directly_observed_has_strong_fixed_equivocation, Ht.
@@ -624,7 +626,7 @@ Lemma fixed_output_has_strong_fixed_equivocation
   l s iom sf om
   (Ht : input_valid_transition Fixed l (s, iom) (sf, Some om))
   : strong_fixed_equivocation IM equivocators sf om.
-Proof.
+Proof using H7.
   apply input_valid_transition_origin in Ht as Hs.
   apply fixed_output_has_strong_fixed_equivocation_helper with s sf l iom.
   - intros m Hobs. apply in_futures_preserves_strong_fixed_equivocation with s.
@@ -679,7 +681,7 @@ Lemma Equivocators_Fixed_Strong_incl base_s
   : VLSM_incl
       (equivocators_composition_for_directly_observed IM equivocators base_s)
       (equivocators_composition_for_sent IM equivocators base_s).
-Proof.
+Proof using H7.
   apply basic_VLSM_incl.
   - by intros s Hincl.
   - intros l s m Hv HsY [Hinit | Hobs]
@@ -695,7 +697,7 @@ Lemma Equivocators_Fixed_Strong_eq base_s
   : VLSM_eq
       (equivocators_composition_for_directly_observed IM equivocators base_s)
       (equivocators_composition_for_sent IM equivocators base_s).
-Proof.
+Proof using H7.
   apply VLSM_eq_incl_iff. split.
   - by apply Equivocators_Fixed_Strong_incl.
   - by apply Equivocators_Strong_Fixed_incl.
@@ -709,7 +711,7 @@ Lemma fixed_strong_equivocation_subsumption
   : input_valid_constraint_subsumption IM
     (fixed_equivocation_constraint IM equivocators)
     (strong_fixed_equivocation_constraint IM equivocators).
-Proof.
+Proof using H7.
   intros l (s, om) Hv.
   destruct om as [m |]; [| done].
   apply proj1 in Hv as Hs.
@@ -717,12 +719,12 @@ Proof.
 Qed.
 
 Lemma Fixed_incl_StrongFixed : VLSM_incl Fixed StrongFixed.
-Proof.
+Proof using H7.
   apply constraint_subsumption_incl. apply fixed_strong_equivocation_subsumption.
 Qed.
 
 Lemma Fixed_eq_StrongFixed : VLSM_eq Fixed StrongFixed.
-Proof.
+Proof using H7.
   apply VLSM_eq_incl_iff. split.
   - by apply Fixed_incl_StrongFixed.
   - by apply StrongFixed_incl_Fixed.
@@ -878,7 +880,7 @@ Context
 Lemma fixed_equivocator_lifting_initial_state :
   weak_projection_initial_state_preservation EquivPreloadedBase Fixed
     (lift_sub_state_to IM (elements equivocators) base_s).
-Proof.
+Proof using Hbase_s H7.
   intros eqv_is Heqv_is.
   apply (VLSM_incl_valid_state (StrongFixed_incl_Fixed IM equivocators)).
   apply (VLSM_projection_valid_state (remove_equivocating_transitions_fixed_projection _ Heqv_is)).
@@ -925,7 +927,7 @@ Lemma EquivPreloadedBase_Fixed_weak_embedding
     forall i m, i ∈ equivocators -> ~ vinitial_message_prop (IM i) m)
   : VLSM_weak_embedding EquivPreloadedBase Fixed
       (lift_sub_label IM (elements equivocators)) (lift_sub_state_to IM (elements equivocators) base_s).
-Proof.
+Proof using Hbase_s H7 H6 H4 H3 H2 H1 H0.
   apply basic_VLSM_weak_embedding.
   - intros l s om Hv HsY HomY. split.
     + destruct Hv as [_ [_ [Hv _]]]; revert Hv; destruct l as (i, li).
@@ -985,7 +987,7 @@ Context
 Lemma strong_fixed_equivocation_no_equivocators
   : forall s m,
   strong_fixed_equivocation IM (@empty Ci _) s m <-> composite_has_been_sent IM s m.
-Proof.
+Proof using H6 H4 H3 H2 H1 H.
   intros s m.
   split.
   - intros [Hsent | Hemit].
@@ -1002,7 +1004,7 @@ Lemma strong_fixed_equivocation_constraint_no_equivocators
   : forall l som,
     strong_fixed_equivocation_constraint IM (@empty Ci _) l som <->
     composite_no_equivocations IM l som.
-Proof.
+Proof using H6 H4 H3 H2 H1 H.
   intros.
   destruct som as (s, [m |]); [| done].
   simpl.
@@ -1014,7 +1016,7 @@ Qed.
 Lemma strong_fixed_equivocation_vlsm_composition_no_equivocators
   : VLSM_eq (strong_fixed_equivocation_vlsm_composition IM (@empty Ci _))
       (composite_vlsm IM (composite_no_equivocations IM)).
-Proof.
+Proof using H6 H4 H3 H2 H1 H.
   apply VLSM_eq_incl_iff.
   split.
   - apply constraint_subsumption_incl.
@@ -1032,7 +1034,7 @@ Qed.
 Lemma fixed_equivocation_vlsm_composition_no_equivocators
   : VLSM_eq (fixed_equivocation_vlsm_composition IM (@empty Ci _))
       (composite_vlsm IM (composite_no_equivocations IM)).
-Proof.
+Proof using H7 H6 H4 H3 H2 H1 H.
   eapply VLSM_eq_trans.
   - by apply Fixed_eq_StrongFixed.
   - by apply strong_fixed_equivocation_vlsm_composition_no_equivocators.
@@ -1070,7 +1072,7 @@ Lemma lift_strong_fixed_non_equivocating
   : VLSM_embedding StrongFixedNonEquivocating StrongFixed
     (lift_sub_label IM (elements non_equivocators))
     (lift_sub_state IM (elements non_equivocators)).
-Proof.
+Proof using H6 H3 H EqDecision0.
   apply induced_sub_projection_lift.
   intros s1 s2 Heq l om.
   destruct om as [m |]; [| by itauto].
@@ -1107,7 +1109,7 @@ Lemma lift_fixed_non_equivocating
   : VLSM_embedding FixedNonEquivocating Fixed
     (lift_sub_label IM (elements non_equivocators))
     (lift_sub_state IM (elements non_equivocators)).
-Proof.
+Proof using H6 H3 H EqDecision0.
   constructor.
   intros sX trX Htr.
   apply
@@ -1124,7 +1126,7 @@ Lemma fixed_non_equivocating_projection_friendliness
   : projection_friendly_prop
       (induced_sub_projection_is_projection IM (elements non_equivocators)
         (fixed_equivocation_constraint IM equivocators)).
-Proof.
+Proof using H6 H3 H EqDecision0.
   apply induced_sub_projection_friendliness.
   by apply lift_fixed_non_equivocating.
 Qed.
@@ -1140,7 +1142,7 @@ Lemma fixed_non_equivocating_traces_char is tr
     finite_valid_trace Fixed eis etr /\
     composite_state_sub_projection IM (elements non_equivocators) eis = is /\
     finite_trace_sub_projection IM (elements non_equivocators) etr = tr.
-Proof.
+Proof using H6 H3 H EqDecision0.
   apply (projection_friendly_trace_char (induced_sub_projection_is_projection _ _ _)).
   by apply fixed_non_equivocating_projection_friendliness.
 Qed.
diff --git a/theories/VLSM/Core/Equivocation/FullNode.v b/theories/VLSM/Core/Equivocation/FullNode.v
index 3bc1f81a..a1ac3fed 100644
--- a/theories/VLSM/Core/Equivocation/FullNode.v
+++ b/theories/VLSM/Core/Equivocation/FullNode.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections Composition.
 From VLSM.Core Require Import Equivocation.
 
+Set Default Proof Using "Type".
+
 Section sec_full_node_constraint.
 
 Context
@@ -95,7 +97,7 @@ Lemma node_generated_without_further_equivocation_weaken
   (m : message)
   (Hsmi : node_generated_without_further_equivocation s m i)
   : node_generated_without_further_equivocation_alt s m i.
-Proof.
+Proof using EqDecision0.
   destruct Hsmi as [si [Hsim Hsi]].
   apply can_emit_iff. exists si.
   revert Hsim.
@@ -112,7 +114,7 @@ Lemma full_node_condition_for_admissible_equivocators_subsumption
   : preloaded_constraint_subsumption IM
       full_node_condition_for_admissible_equivocators
       full_node_condition_for_admissible_equivocators_alt.
-Proof.
+Proof using EqDecision0.
   intros l (s, [m |]) [Hs [_ [_ Hc]]]; [| done].
   destruct Hc as [Hno_equiv | Hfull]; [by left |].
   right.
diff --git a/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v b/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v
index 829a8d1d..f604bcce 100644
--- a/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/LimitedMessageEquivocation.v
@@ -8,6 +8,8 @@ From VLSM.Core Require Import Equivocation.FixedSetEquivocation.
 From VLSM.Core Require Import Equivocation.TraceWiseEquivocation.
 From VLSM.Core Require Import Equivocation.WitnessedEquivocation.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Limited Message Equivocation
 
   In this section we define the notion of limited (message-based) equivocation.
@@ -64,7 +66,7 @@ Definition limited_equivocation_composite_vlsm : VLSM message :=
 Lemma limited_equivocation_valid_state s
   : valid_state_prop limited_equivocation_composite_vlsm s ->
     LimitedEquivocationProp s.
-Proof.
+Proof using Hno_initial_equivocation H7 H6 H4 H3 H2 H1 H0 EqDecision1.
   intros Hs; apply valid_state_prop_iff in Hs
     as [[[is His] ->] | (l & [s' om'] & om & [(_ & _ & _ & Hv) Ht])]; simpl.
   - exists ∅.
@@ -210,7 +212,7 @@ Context
 Lemma StrongFixed_valid_state_not_heavy s
   (Hs : valid_state_prop StrongFixed s)
   : tracewise_not_heavy s.
-Proof.
+Proof using Inj0 Hsender_safety Hlimited H7 H6 H4 H3 H.
   cut (tracewise_equivocating_validators s ⊆ eqv_validators).
   {
     intro Hincl; unfold tracewise_not_heavy, not_heavy.
@@ -249,7 +251,7 @@ Proof.
 Qed.
 
 Lemma StrongFixed_incl_Limited : VLSM_incl StrongFixed Limited.
-Proof.
+Proof using Inj0 Hsender_safety Hlimited H7 H6 H4 H3 H.
   apply constraint_subsumption_incl.
   intros [i li] [s om] Hpv.
   unfold limited_equivocation_constraint.
@@ -259,7 +261,7 @@ Proof.
 Qed.
 
 Lemma Fixed_incl_Limited : VLSM_incl Fixed Limited.
-Proof.
+Proof using Inj0 Hsender_safety Hlimited H7 H6 H4 H3 H.
   specialize (Fixed_eq_StrongFixed IM equivocators)
     as Heq.
   apply VLSM_eq_proj1 in Heq.
@@ -318,7 +320,7 @@ Context
 Lemma traces_exhibiting_limited_equivocation_are_valid
   (Hsender_safety : sender_safety_alt_prop IM A sender)
   : forall s tr, fixed_limited_equivocation_prop s tr -> finite_valid_trace Limited s tr.
-Proof.
+Proof using Inj0 H7 H6 H4 H3 H.
   intros s tr [equivocators [Hlimited Htr]].
   eapply VLSM_incl_finite_valid_trace; [| done].
   by eapply Fixed_incl_Limited.
@@ -343,7 +345,7 @@ Lemma traces_exhibiting_limited_equivocation_are_valid_rev
     finite_valid_trace_init_to (free_composite_vlsm IM) is s tr ->
     tracewise_not_heavy s ->
     fixed_limited_equivocation_prop is tr.
-Proof.
+Proof using H7 H6 H4 H3 H.
   intros is s tr Hstrong Htr Hnot_heavy.
   exists (equivocating_validators s).
   split; cycle 1.
@@ -365,7 +367,7 @@ Lemma limited_traces_exhibiting_limited_equivocation_are_valid_rev
   (can_emit_signed : channel_authentication_prop IM A sender)
   : forall s tr, strong_trace_witnessing_equivocation_prop IM threshold A sender s tr (Cv := Cv) ->
     finite_valid_trace Limited s tr -> fixed_limited_equivocation_prop s tr.
-Proof.
+Proof using H7 H6 H4 H3 H.
   intros s tr Hstrong Htr.
   eapply traces_exhibiting_limited_equivocation_are_valid_rev; [done.. | |].
   - apply valid_trace_add_default_last.
@@ -390,7 +392,7 @@ Lemma limited_valid_state_has_trace_exhibiting_limited_equivocation
   (can_emit_signed : channel_authentication_prop IM A sender)
   : forall s, valid_state_prop Limited s ->
     exists is tr, finite_trace_last is tr = s /\ fixed_limited_equivocation_prop is tr.
-Proof.
+Proof using H7 H6 H4 H3 H.
   intros s Hs.
   assert (Hfree_s : valid_state_prop (free_composite_vlsm IM) s)
     by (revert Hs; apply VLSM_incl_valid_state, constraint_free_incl).
diff --git a/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v b/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v
index d6cd0e88..b1d374ff 100644
--- a/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v
+++ b/theories/VLSM/Core/Equivocation/MinimalEquivocationTrace.v
@@ -3,6 +3,8 @@ From VLSM.Lib Require Import Preamble ListExtras StdppListSet StdppExtras NatExt
 From VLSM.Core Require Import VLSM Composition.
 From VLSM.Core Require Import Equivocation MessageDependencies TraceableVLSM.
 
+Set Default Proof Using "Type".
+
 (** * Minimally-equivocating traces
 
   In this module we define a [choice_function], [minimal_equivocation_choice],
@@ -99,7 +101,7 @@ Lemma not_CompositeNthSentNotObserved_is_observed :
       ts !! n = Some (item, s) ->
       forall m, output item = Some m ->
       CompositeHasBeenObserved IM message_dependencies s m.
-Proof.
+Proof using full_message_dependencies H11 H EqDecision1.
   intros * Hnobs **.
   destruct (decide (CompositeHasBeenObserved IM message_dependencies s m)); [done |].
   by contradict Hnobs; econstructor.
@@ -115,7 +117,7 @@ Definition composite_latest_sent_not_observed_prop
 
 #[local] Instance composite_latest_sent_not_observed_dec s' :
   RelDecision (composite_latest_sent_not_observed_prop s').
-Proof.
+Proof using full_message_dependencies H11 H.
   intros i n.
   destruct (composite_state_destructor IM state_destructor s' i !! n)
     as [[item s] |] eqn: Hdestruct;
@@ -194,7 +196,7 @@ Qed.
 
 #[local] Instance latest_composite_observed_before_send_irreflexive s' :
   Irreflexive (latest_composite_observed_before_send s').
-Proof.
+Proof using Irreflexive0.
   intros a (s_i & item_i & m_i & s_j & item_j & m_j & [Hdestruct Houtput H_destruct H_output Hrel]).
   rewrite Hdestruct in H_destruct; inversion H_destruct; subst; clear H_destruct.
   rewrite Houtput in H_output; inversion H_output; subst.
@@ -210,7 +212,7 @@ Lemma composite_latest_sent_observed_in_before_send
     head (composite_state_destructor IM state_destructor s' j) = Some (item_j, s_j) ->
     output item_j = Some m_j ->
     latest_composite_observed_before_send s' i j.
-Proof.
+Proof using validator state_size sender full_message_dependencies Hchannel H13 H12 H11 A.
   intros Hs' Hdestruct_j Houtput_j.
   eapply composite_state_destructor_head_reachable in Hdestruct_j as Htj; [| done..].
   destruct Hij as [Hdestruct_i Houtput_i Hobs].
@@ -273,7 +275,7 @@ Lemma traceable_vlsm_initial_state_dec :
   forall (i : index) (si : vstate (IM i)),
     valid_state_prop (pre_loaded_with_all_messages_vlsm (IM i)) si ->
     Decision (vinitial_state_prop (IM i) si).
-Proof.
+Proof using state_size state_destructor H13.
   intros; destruct (decide (state_destructor i si = nil)).
   - by left; apply tv_state_destructor_initial.
   - by right; contradict n; apply tv_state_destructor_initial.
@@ -456,7 +458,7 @@ Lemma all_latest_composite_observed_before_send_one_step
     forall isj, is' !! j = Some isj ->
     forall isi, is' !! (S j) = Some isi ->
     latest_composite_observed_before_send s isi isj.
-Proof.
+Proof using validator state_size sender full_message_dependencies Hchannel H13 H12 H11 A.
   intros Hall j isj Hisj isi Hisi.
   eapply ForAllSuffix2_lookup in Hisj as Hobs_j; [| done..].
   destruct Hobs_j as (s_isi & item_isi & m_isi & Hobs_j).
@@ -483,7 +485,7 @@ Lemma all_latest_composite_observed_before_send
     forall isi, is' !! i = Some isi ->
     forall isj, is' !! j = Some isj ->
     latest_composite_observed_before_send s isi isj.
-Proof.
+Proof using validator state_size sender full_message_dependencies Hchannel H13 H12 H11 A.
   intros Hall i j Hij; unfold gt, lt in Hij; remember (S j) as k.
   revert j Heqk; induction Hij; intros j -> isi Hisi isj Hisj.
   - by eapply all_latest_composite_observed_before_send_one_step.
@@ -530,7 +532,7 @@ Lemma at_least_one_send_not_previously_observed
     find_not_send_decomposition s' is = None ->
     find_sent_not_observed_decomposition s' is = None ->
       False.
-Proof.
+Proof using validator sender Irreflexive0 Hchannel H12 A.
   intros Hinitial Hnot_send Hsent_not_obs.
   assert (Hall_sent_observed :
     forall x : index, x ∈ is ->
@@ -592,7 +594,7 @@ Lemma minimal_equivocation_choice_monotone :
         forall v : validator,
           msg_dep_is_globally_equivocating IM message_dependencies sender s v ->
           msg_dep_is_globally_equivocating IM message_dependencies sender s' v.
-Proof.
+Proof using Irreflexive0 Hchannel H12 A.
   intros is Hnodup s' Hs' Hnis i Hi n Hchoice s item Hdestruct v [m []].
   eapply composite_state_destructor_lookup_reachable in Hdestruct as Ht;
     [| typeclasses eauto | done].
@@ -692,7 +694,7 @@ Lemma state_to_minimal_equivocation_trace_equivocation_monotonic :
         (finite_trace_last is pre) v ->
       msg_dep_is_globally_equivocating IM message_dependencies sender
         (destination item) v.
-Proof.
+Proof using Irreflexive0 Hchannel H12 A.
   intros.
   eapply composite_state_to_trace_P_monotonic with
     (P := fun s => msg_dep_is_globally_equivocating IM message_dependencies sender s v);
diff --git a/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v b/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v
index 55bf69d8..07c5c6e7 100644
--- a/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/MsgDepFixedSetEquivocation.v
@@ -4,6 +4,8 @@ From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM MessageDependencies VLSMProjections Composition Equivocation.
 From VLSM.Core Require Import Equivocation.FixedSetEquivocation ProjectionTraces SubProjectionTraces.
 
+Set Default Proof Using "Type".
+
 Section sec_msg_dep_fixed_set_equivocation.
 
 Context
@@ -48,7 +50,7 @@ Lemma messages_with_valid_dependences_can_be_emitted s dm
   (Hdm_i : dm_i ∈ equivocators)
   (Hemitted : can_emit (pre_loaded_with_all_messages_vlsm (IM dm_i)) dm)
   : can_emit (equivocators_composition_for_sent IM equivocators s) dm.
-Proof.
+Proof using Irreflexive0 H9 H8 H18 H17 H14 H12 H11 H10.
   eapply sub_valid_preloaded_lifts_can_be_emitted, message_dependencies_are_sufficient.
   - by apply elem_of_elements, Hdm_i.
   - by apply Hdepm.
@@ -73,7 +75,7 @@ Lemma dependencies_are_valid s m
     forall dm, msg_dep_rel message_dependencies dm m ->
       valid_message_prop
         (equivocators_composition_for_sent IM equivocators s) dm.
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10.
   induction m as [m Hind] using (well_founded_ind Hmsg_dep_happens_before_wf).
   intros Heqv dm Hdm.
   apply emitted_messages_are_valid_iff.
@@ -93,7 +95,7 @@ Lemma msg_dep_strong_fixed_equivocation_subsumption s m
   (Hmsg_dep_happens_before_wf : well_founded (msg_dep_happens_before message_dependencies))
   : msg_dep_fixed_set_equivocation s m ->
     strong_fixed_equivocation IM equivocators s m.
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10.
   intros  [Hsent | [[i [Hi Hemit]] Heqv]]; [by left |].
   cut (forall dm, msg_dep_rel message_dependencies dm m ->
     valid_message_prop (equivocators_composition_for_sent IM equivocators s) dm)
@@ -108,7 +110,7 @@ Lemma msg_dep_strong_fixed_equivocation_constraint_subsumption
   : strong_constraint_subsumption IM
       msg_dep_fixed_set_equivocation_constraint
       (strong_fixed_equivocation_constraint IM equivocators).
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10.
   intros l [s [m |]] Hc; [| done].
   by apply msg_dep_strong_fixed_equivocation_subsumption.
 Qed.
@@ -172,7 +174,7 @@ Lemma sent_by_non_equivocating_msg_dep_rel_strong_fixed_equivocation
     forall dm m, msg_dep_rel message_dependencies dm m ->
     sent_by_non_equivocating  IM equivocators s m ->
     strong_fixed_equivocation IM equivocators s dm.
-Proof.
+Proof using Irreflexive0 H18 H17.
   intros s Hs dm m Hdm (i & Hni & Hsent).
   apply (messages_sent_from_component_produced_previously IM Hs) in Hsent
     as (destination & Hfutures & Hproduce).
@@ -206,7 +208,7 @@ Lemma msg_dep_rel_reflects_strong_fixed_equivocation
     forall dm m, msg_dep_rel message_dependencies dm m ->
     strong_fixed_equivocation IM equivocators s m ->
     strong_fixed_equivocation IM equivocators s dm.
-Proof.
+Proof using Irreflexive0 H18 H17.
   intros s Hs dm m Hdm [Hsent | Hemit].
   - by eapply sent_by_non_equivocating_msg_dep_rel_strong_fixed_equivocation.
   - cut (valid_message_prop (equivocators_composition_for_sent IM equivocators s) dm).
@@ -235,7 +237,7 @@ Lemma strong_fixed_equivocation_msg_dep_constraint_subsumption
   : input_valid_constraint_subsumption IM
       (strong_fixed_equivocation_constraint IM equivocators)
       msg_dep_fixed_set_equivocation_constraint.
-Proof.
+Proof using Irreflexive0 H18 H17.
   intros l [s [m |]] (Hs & _ & _ & Hc); [| done].
   cut (dependencies_with_non_equivocating_senders_were_sent s m).
   {
@@ -259,7 +261,7 @@ Lemma msg_dep_strong_fixed_equivocation_incl
   : VLSM_incl
       (composite_vlsm IM msg_dep_fixed_set_equivocation_constraint)
       (composite_vlsm IM (strong_fixed_equivocation_constraint IM equivocators)).
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10.
   apply constraint_subsumption_incl.
   apply preloaded_constraint_subsumption_stronger.
   apply strong_constraint_subsumption_strongest.
@@ -271,7 +273,7 @@ Lemma strong_msg_dep_fixed_equivocation_incl
   : VLSM_incl
       (composite_vlsm IM (strong_fixed_equivocation_constraint IM equivocators))
       (composite_vlsm IM msg_dep_fixed_set_equivocation_constraint).
-Proof.
+Proof using Irreflexive0 H18 H17.
   apply constraint_subsumption_incl.
   by apply strong_fixed_equivocation_msg_dep_constraint_subsumption.
 Qed.
@@ -282,7 +284,7 @@ Lemma msg_dep_strong_fixed_equivocation_eq
   : VLSM_eq
       (composite_vlsm IM msg_dep_fixed_set_equivocation_constraint)
       (composite_vlsm IM (strong_fixed_equivocation_constraint IM equivocators)).
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H18 H17 H14 H12 H11 H10.
   apply VLSM_eq_incl_iff; split.
   - by apply msg_dep_strong_fixed_equivocation_incl.
   - by apply strong_msg_dep_fixed_equivocation_incl.
@@ -323,7 +325,7 @@ Lemma msg_dep_full_node_fixed_set_equivocation_constraint_subsumption
   : strong_constraint_subsumption IM
       (msg_dep_fixed_set_equivocation_constraint IM message_dependencies equivocators)
       full_node_fixed_set_equivocation_constraint.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0 EqDecision0.
   intros l [s [m |]]; [| done]
   ; intros [Hsent | [[i [Hi Hemit]] Hdeps]]; [by left | right].
   apply Hchannel in Hemit; cbv in Hemit |- *.
@@ -345,7 +347,7 @@ Lemma fixed_full_node_equivocation_incl
   : VLSM_incl
       (composite_vlsm IM (fixed_equivocation_constraint IM equivocators))
       (composite_vlsm IM full_node_fixed_set_equivocation_constraint).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Irreflexive0 H9 H7 H6 H4 H3 H2 H18 H16 H15 H14 H13 H12 H11 H10 H1 H0 EqDecision1 Cm.
   eapply VLSM_incl_trans.
   - by apply Fixed_incl_StrongFixed.
   - eapply VLSM_incl_trans.
@@ -363,7 +365,7 @@ Lemma full_node_fixed_equivocation_constraint_subsumption
   : input_valid_constraint_subsumption IM
       full_node_fixed_set_equivocation_constraint
       (fixed_equivocation_constraint IM equivocators).
-Proof.
+Proof using no_initial_messages_in_IM Irreflexive0 H6 H4 H3 H2 H18 H1 H0.
   intros l [s [m |]] (_ & Hm & Hv & Hc); [| itauto]
   ; destruct Hc as [Hsent | Heqv]; [left | right].
   - by revert Hsent; apply sent_by_non_equivocating_are_directly_observed.
@@ -406,7 +408,7 @@ Lemma full_node_fixed_equivocation_incl
   : VLSM_incl
       (composite_vlsm IM full_node_fixed_set_equivocation_constraint)
       (composite_vlsm IM (fixed_equivocation_constraint IM equivocators)).
-Proof.
+Proof using no_initial_messages_in_IM Irreflexive0 H6 H4 H3 H2 H18 H1 H0.
   apply constraint_subsumption_incl.
   by apply full_node_fixed_equivocation_constraint_subsumption.
 Qed.
@@ -417,7 +419,7 @@ Lemma full_node_fixed_equivocation_eq
   : VLSM_eq
       (composite_vlsm IM full_node_fixed_set_equivocation_constraint)
       (composite_vlsm IM (fixed_equivocation_constraint IM equivocators)).
-Proof.
+Proof using no_initial_messages_in_IM Irreflexive0 H7 H6 H4 H3 H2 H18 H1 H0.
   apply VLSM_eq_incl_iff; split.
   - apply full_node_fixed_equivocation_incl; [done |].
     by apply channel_authentication_sender_safety.
diff --git a/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v b/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v
index 61200887..3758d36c 100644
--- a/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/MsgDepLimitedEquivocation.v
@@ -10,6 +10,8 @@ From VLSM.Core Require Import Equivocation.LimitedMessageEquivocation.
 From VLSM.Core Require Import Equivocation.MsgDepFixedSetEquivocation.
 From VLSM.Core Require Import Equivocation.TraceWiseEquivocation.
 
+Set Default Proof Using "Type".
+
 (**
   To allow capturing the two models of limited equivocation described in the
   sections below, we first define a notion of limited equivocation parameterized
@@ -72,7 +74,7 @@ Definition coeqv_annotate_trace_with_equivocators :=
 Lemma coeqv_limited_equivocation_transition_state_annotation_incl [l s iom s' oom]
   : vtransition coeqv_limited_equivocation_vlsm l (s, iom) = (s', oom) ->
     state_annotation s ⊆ state_annotation s'.
-Proof.
+Proof using H7 H5 H4 EqDecision1.
   cbn; unfold annotated_transition; destruct (vtransition _ _ _) as (_s', _om').
   inversion 1; cbn.
   by destruct iom as [m |]; [apply union_subseteq_l |].
@@ -81,7 +83,7 @@ Qed.
 Lemma coeqv_limited_equivocation_state_annotation_nodup s
   : valid_state_prop coeqv_limited_equivocation_vlsm s ->
     NoDup (elements (state_annotation s)).
-Proof.
+Proof using H7 H5 H4 H0 EqDecision1.
   induction 1 using valid_state_prop_ind.
   - by destruct s, Hs as [_ ->]; cbn in *; apply NoDup_elements.
   - destruct Ht as [_ Ht]; cbn in Ht.
@@ -92,7 +94,7 @@ Qed.
 Lemma coeqv_limited_equivocation_state_not_heavy s
   : valid_state_prop coeqv_limited_equivocation_vlsm s ->
     (sum_weights (state_annotation s) <= threshold)%R.
-Proof.
+Proof using H8 H7 H5 H4 H0 EqDecision1.
   induction 1 using valid_state_prop_ind.
   - destruct s, Hs as [_ ->]; cbn in *.
     rewrite sum_weights_empty; [| done].
@@ -235,7 +237,7 @@ Context
 Lemma full_node_msg_dep_coequivocating_senders s m i li
   (Hvalid : input_valid (pre_loaded_with_all_messages_vlsm (IM i)) li (s i, Some m))
   : msg_dep_coequivocating_senders IM full_message_dependencies sender s m ≡@{Cv} ∅.
-Proof.
+Proof using message_dependencies Hfull H6 H4 H3 H19 H17 H16 H15 H14 H FullMessageDependencies0 EqDecision2 EqDecision0.
   intro; split; intro Hx; [| by contradict Hx; apply not_elem_of_empty].
   exfalso; contradict Hx.
   unfold msg_dep_coequivocating_senders.
@@ -273,7 +275,7 @@ Lemma full_node_msg_dep_composite_transition_message_equivocators
     msg_dep_composite_transition_message_equivocators
       IM full_message_dependencies sender
       (existT i li) (s, om).
-Proof.
+Proof using message_dependencies Hfull H6 H4 H3 H19 H17 H15 H14 H FullMessageDependencies0 EqDecision2 EqDecision0.
   destruct om as [m |]; cbn; [| done].
   apply sets.union_proper; [done |].
   unfold coeqv_message_equivocators, msg_dep_coequivocating_senders.
@@ -288,7 +290,7 @@ Lemma msg_dep_full_node_valid_iff
   (Hvi : input_valid (pre_loaded_with_all_messages_vlsm (IM (projT1 l)))
            (projT2 l) (original_state s (projT1 l), om))
   : vvalid Limited l (s, om) <-> vvalid FullNodeLimited l (s, om).
-Proof.
+Proof using message_dependencies Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0.
   cbn; unfold annotated_valid, coeqv_limited_equivocation_constraint; destruct l as [i li].
   replace (sum_weights _) with
     (sum_weights
@@ -304,7 +306,7 @@ Lemma msg_dep_full_node_transition_iff
   (Hvi : input_valid (pre_loaded_with_all_messages_vlsm (IM (projT1 l)))
            (projT2 l) (original_state s (projT1 l), om))
   : vtransition Limited l (s, om) = vtransition FullNodeLimited l (s, om).
-Proof.
+Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0.
   cbn; unfold annotated_transition;
     destruct (vtransition _ _ _) as (s', om'), l as (i, li).
   do 2 f_equal.
@@ -315,7 +317,7 @@ Qed.
 
 Lemma msg_dep_full_node_limited_equivocation_vlsm_incl :
   VLSM_incl Limited FullNodeLimited.
-Proof.
+Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0.
   apply basic_VLSM_incl.
   - by intros s Hs.
   - by intros _ _ m _ _ Hinit; apply initial_message_is_valid.
@@ -329,7 +331,7 @@ Qed.
 
 Lemma full_node_msg_dep_limited_equivocation_vlsm_incl :
   VLSM_incl FullNodeLimited Limited.
-Proof.
+Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0.
   apply basic_VLSM_incl.
   - by intros s Hs.
   - by intros _ _ m _ _ Hinit; apply initial_message_is_valid.
@@ -343,7 +345,7 @@ Qed.
 
 Lemma full_node_msg_dep_limited_equivocation_vlsm_eq :
   VLSM_eq FullNodeLimited Limited.
-Proof.
+Proof using message_dependencies LeibnizEquiv0 Hfull H6 H4 H3 H19 H17 H15 H14 H10 H FullMessageDependencies0 EqDecision2 EqDecision0.
   apply VLSM_eq_incl_iff; split.
   - by apply full_node_msg_dep_limited_equivocation_vlsm_incl.
   - by apply msg_dep_full_node_limited_equivocation_vlsm_incl.
@@ -385,7 +387,7 @@ Lemma equivocating_messages_are_equivocator_emitted
       v ∈ msg_dep_message_equivocators IM full_message_dependencies sender s im (Cv := Cv)
         /\
       can_emit (pre_loaded_vlsm (IM (A v)) (fun dm => msg_dep_rel message_dependencies dm im)) im.
-Proof.
+Proof using Hchannel H26 H24 H23 H18 FullMessageDependencies0 EqDecision2.
   eapply (VLSM_incl_can_emit (vlsm_incl_pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM)))
       in Him.
   apply can_emit_composite_project in Him as [j Him].
@@ -410,7 +412,7 @@ Lemma equivocating_messages_dependencies_are_directly_observed_or_equivocator_em
     composite_has_been_directly_observed IM s dm \/
     exists v_i, v_i ∈ msg_dep_message_equivocators IM full_message_dependencies sender s im (Cv := Cv) /\
       can_emit (pre_loaded_with_all_messages_vlsm (IM (A v_i))) dm.
-Proof.
+Proof using no_initial_messages_in_IM Hchannel H26 H24 H23 H18 FullMessageDependencies0 EqDecision2.
   intros dm Hdm.
   destruct (decide (composite_has_been_directly_observed IM s dm)) as [Hobs | Hnobs]
   ; [by left | right].
@@ -444,7 +446,7 @@ Lemma message_equivocators_can_emit (s : vstate Limited) im
                 (original_state s) im))
         (original_state s))
       im.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Hsender_safety Hchannel H8 H6 H4 H3 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1.
   eapply VLSM_embedding_can_emit.
   - unshelve apply equivocators_composition_for_directly_observed_index_incl_embedding with
       (indices1 := fin_sets.set_map A (msg_dep_message_equivocators IM (Cv := Cv)
@@ -487,7 +489,7 @@ Lemma msg_dep_fixed_limited_equivocation_witnessed
       (pre_VLSM_embedding_finite_trace_project
         (type Limited) (composite_type IM) Datatypes.id original_state
         tr).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Hsender_safety Hchannel H8 H6 H4 H3 H27 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1.
   repeat split; [.. | by apply Htr].
   - by eapply coeqv_limited_equivocation_state_not_heavy,
             finite_valid_trace_last_pstate, Htr.
@@ -581,7 +583,7 @@ Corollary msg_dep_fixed_limited_equivocation is tr
       (pre_VLSM_embedding_finite_trace_project
         (type Limited) (composite_type IM) Datatypes.id original_state
         tr) (Ci := Ci) (Cv := Cv).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Hsender_safety Hchannel H8 H6 H4 H3 H27 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1.
   intro Htr.
   exists (state_annotation (finite_trace_last is tr)).
   by apply msg_dep_fixed_limited_equivocation_witnessed.
@@ -614,7 +616,7 @@ Lemma fixed_transition_preserves_annotation_equivocators
           (msg_dep_composite_transition_message_equivocators IM full_message_dependencies sender)
           {| original_state := is; state_annotation := empty_set |} tr), iom)
     ⊆ eqv_validators.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Inj0 Hsender_safety Hchannel H8 H6 H4 H3 H26 H24 H23 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1.
   destruct iom as [im |]; [| done].
   apply ListFinSetExtras.set_union_subseteq_iff; split; [done | cbn].
   rewrite annotate_trace_from_last_original_state; cbn.
@@ -672,7 +674,7 @@ Lemma msg_dep_limited_fixed_equivocation
     finite_valid_trace Limited
       {| original_state := is; state_annotation := ` inhabitant |}
       (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender is tr).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Inj0 Hsender_safety Hchannel H8 H6 H4 H3 H26 H24 H23 H19 H18 H15 H13 H12 H FullMessageDependencies0 EqDecision2 EqDecision1.
   intros (equivocators & Hlimited & Htr).
   split; [| by split; [apply Htr |]].
   apply valid_trace_add_default_last in Htr.
@@ -733,7 +735,7 @@ Lemma annotated_limited_incl_constrained_limited
       Limited
       (tracewise_limited_equivocation_vlsm_composition IM threshold A sender (Cv := Cv))
       Datatypes.id original_state.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Inj0 Hsender_safety Hchannel H8 H6 H5 H4 H3 H2 H18 H15 H13 H12 H1 H0 H FullMessageDependencies0 EqDecision1 Ci.
   constructor; intros sX trX HtrX.
   eapply @traces_exhibiting_limited_equivocation_are_valid; [done.. | |].
   - by apply Hsender_safety.
diff --git a/theories/VLSM/Core/Equivocation/NoEquivocation.v b/theories/VLSM/Core/Equivocation/NoEquivocation.v
index 3b89a5d7..71dfd06d 100644
--- a/theories/VLSM/Core/Equivocation/NoEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/NoEquivocation.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation.
 
+Set Default Proof Using "Type".
+
 (** * VLSM No Equivocation Composition Constraints *)
 
 Section sec_no_equivocations.
@@ -84,7 +86,7 @@ Lemma directly_observed_were_sent_preserved l s im s' om :
   input_valid_transition X l (s, im) (s', om) ->
   directly_observed_were_sent s ->
   directly_observed_were_sent s'.
-Proof.
+Proof using Henforced.
   intros Hptrans Hprev msg Hobs.
   specialize (Hprev msg).
   apply preloaded_weaken_input_valid_transition in Hptrans.
@@ -105,7 +107,7 @@ Qed.
 Lemma directly_observed_were_sent_invariant s:
   valid_state_prop X s ->
   directly_observed_were_sent s.
-Proof.
+Proof using Henforced.
   intro Hproto.
   induction Hproto using valid_state_prop_ind.
   - by apply directly_observed_were_sent_initial.
@@ -122,7 +124,7 @@ Lemma no_equivocations_preloaded_traces
   (is : state)
   (tr : list transition_item)
   : finite_valid_trace (pre_loaded_with_all_messages_vlsm X) is tr -> finite_valid_trace X is tr.
-Proof.
+Proof using Henforced H0 H.
   intro Htr.
   induction Htr using finite_valid_trace_rev_ind.
   - split; [| done].
@@ -142,7 +144,7 @@ Qed.
 
 Lemma preloaded_incl_no_equivocations
   : VLSM_incl (pre_loaded_with_all_messages_vlsm X) X.
-Proof.
+Proof using Henforced H0 H.
   specialize no_equivocations_preloaded_traces.
   clear -X. destruct X as [T [S M]].
   by apply VLSM_incl_finite_traces_characterization.
@@ -150,7 +152,7 @@ Qed.
 
 Lemma preloaded_eq_no_equivocations
   : VLSM_eq (pre_loaded_with_all_messages_vlsm X) X.
-Proof.
+Proof using Henforced H0 H.
   specialize preloaded_incl_no_equivocations.
   specialize (vlsm_incl_pre_loaded_with_all_messages_vlsm X).
   clear -X. destruct X as [T [S M]].
@@ -215,7 +217,7 @@ Definition composite_directly_observed_were_sent (s : state) : Prop :=
 Lemma composite_directly_observed_were_sent_invariant s :
   valid_state_prop X s ->
   composite_directly_observed_were_sent s.
-Proof.
+Proof using Hsubsumed H.
   intros Hs m.
   rewrite composite_has_been_directly_observed_sent_received_iff.
   intros Hobs.
diff --git a/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v b/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v
index c721c158..3d577ff4 100644
--- a/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/TraceWiseEquivocation.v
@@ -6,6 +6,8 @@ From VLSM.Core Require Import VLSM Composition ProjectionTraces.
 From VLSM.Core Require Import Equivocation.
 From VLSM.Lib Require Import Preamble StdppExtras.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Trace-wise Equivocation
 
   In this section we define a more precise notion of message equivocation,
@@ -46,7 +48,7 @@ Definition item_equivocating_in_trace
   := from_option (fun m => ~ trace_has_message (field_selector output) m tr) False (input item).
 
 #[local] Instance item_equivocating_in_trace_dec : RelDecision item_equivocating_in_trace.
-Proof.
+Proof using EqDecision0.
   intros item tr.
   destruct item. destruct input as [m |]; [| by right; itauto].
   unfold item_equivocating_in_trace, trace_has_message, field_selector; cbn.
@@ -126,7 +128,7 @@ Qed.
 
 Lemma equivocating_senders_in_trace_prefix prefix suffix
   : equivocating_senders_in_trace prefix ⊆ equivocating_senders_in_trace (prefix ++ suffix).
-Proof.
+Proof using PreFree EqDecision1.
   intros v. rewrite !elem_of_equivocating_senders_in_trace.
   intros [m [Hm Heqv]].
   exists m. split; [done |].
@@ -226,7 +228,7 @@ Lemma transition_is_equivocating_tracewise_char
   : is_equivocating_tracewise_no_has_been_sent s' v ->
     is_equivocating_tracewise_no_has_been_sent s v \/
     option_bind _ _ sender om = Some v.
-Proof.
+Proof using EqDecision4.
   destruct (decide (option_bind _ _ sender om = Some v))
   ; [by intro; right |].
   intros Heqv. left. intros is tr [Htr Hinit].
@@ -249,7 +251,7 @@ Lemma transition_receiving_no_sender_reflects_is_equivocating_tracewise
   (Hno_sender : option_bind _ _ sender om = None)
   (v : validator)
   : is_equivocating_tracewise_no_has_been_sent s' v -> is_equivocating_tracewise_no_has_been_sent s v.
-Proof.
+Proof using EqDecision4.
   intro Hs'.
   by destruct (transition_is_equivocating_tracewise_char _ _ _ _ _ Ht v Hs'); [| congruence].
 Qed.
diff --git a/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v b/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v
index faf5343c..b3848208 100644
--- a/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v
+++ b/theories/VLSM/Core/Equivocation/WitnessedEquivocation.v
@@ -5,6 +5,8 @@ From VLSM.Core Require Import VLSM VLSMProjections Composition.
 From VLSM.Core Require Import SubProjectionTraces MessageDependencies Equivocation.
 From VLSM.Core Require Import NoEquivocation FixedSetEquivocation TraceWiseEquivocation.
 
+Set Default Proof Using "Type".
+
 (** * Witnessed equivocation
 
   Although [is_equivocating_tracewise] provides a very precise notion of
@@ -361,7 +363,7 @@ Lemma strong_trace_witnessing_equivocation_prop_extend_eq
   (Hwitness : trace_witnessing_equivocation_prop is (tr' ++ [item]))
   (Heq : equivocating_validators s ≡@{Cv} equivocating_validators (destination item))
   : strong_trace_witnessing_equivocation_prop is' (tr'' ++ [item]).
-Proof.
+Proof using H0 H.
   intros prefix suffix Heq_tr''_item.
   destruct_list_last suffix suffix' sitem Hsuffix_eq.
   - rewrite app_nil_r in Heq_tr''_item.
@@ -475,7 +477,7 @@ Lemma preloaded_has_strong_trace_witnessing_equivocation_prop s
   : exists is' tr',
     finite_valid_trace_init_to PreFree is' s tr' /\
     strong_trace_witnessing_equivocation_prop is' tr'.
-Proof.
+Proof using Hke H0 H.
   apply is_equivocating_tracewise_witness in Hs.
   destruct Hs as [is [tr [Htr Hwitness]]].
   apply finite_valid_trace_init_to_last in Htr as Hlst.
@@ -600,7 +602,7 @@ Lemma free_has_strong_trace_witnessing_equivocation_prop s
   : exists is' tr',
     finite_valid_trace_init_to Free is' s tr' /\
     strong_trace_witnessing_equivocation_prop is' tr'.
-Proof.
+Proof using Hke H1 H0 H.
   apply (VLSM_incl_valid_state (vlsm_incl_pre_loaded_with_all_messages_vlsm Free))
     in Hs as Hpre_s.
   apply preloaded_has_strong_trace_witnessing_equivocation_prop in Hpre_s.
@@ -683,7 +685,7 @@ Lemma equivocators_can_emit_free m
   : can_emit
     (equivocators_composition_for_directly_observed IM (Ci := Ci) (fin_sets.set_map A (equivocating_validators sf)) s)
     m.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H6 H4 H3 H29 H28 H27 H26 H25 H24 H23 H22 H21 H EqDecision3 Cm.
   apply emitted_messages_are_valid_iff in Hmsg
     as [(_v & [_im Him] & Heqim) | Hiom]
   ; [by elim (no_initial_messages_in_IM _v _im) |].
@@ -730,7 +732,7 @@ Lemma strong_witness_has_fixed_equivocation is s tr
   (Heqv : strong_trace_witnessing_equivocation_prop (Cv := Cv) IM threshold A sender is tr)
   : finite_valid_trace_init_to (fixed_equivocation_vlsm_composition IM (Ci := Ci)
       (fin_sets.set_map A (equivocating_validators s))) is s tr.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H7 H6 H4 H3 H29 H28 H27 H26 H25 H24 H23 H22 H21 H Free_has_sender EqDecision3 Cm.
   split; [| by apply Htr].
   induction Htr using finite_valid_trace_init_to_rev_ind.
   - eapply (finite_valid_trace_from_to_empty (fixed_equivocation_vlsm_composition IM
@@ -814,7 +816,7 @@ Lemma equivocating_validators_fixed_equivocation_characterization
     valid_state_prop Free s ->
     valid_state_prop
       (composite_vlsm IM (equivocating_validators_fixed_equivocation_constraint s)) s.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies can_emit_signed Irreflexive0 Hsender_safety Hfull H7 H6 H4 H3 H29 H28 H27 H26 H25 H24 H23 H22 H21 H Free_has_sender EqDecision3 Cm.
   intros s Hs.
   destruct
     (free_has_strong_trace_witnessing_equivocation_prop IM threshold A sender _ s Hs)
diff --git a/theories/VLSM/Core/EquivocationProjections.v b/theories/VLSM/Core/EquivocationProjections.v
index 1d096881..75853c5e 100644
--- a/theories/VLSM/Core/EquivocationProjections.v
+++ b/theories/VLSM/Core/EquivocationProjections.v
@@ -3,6 +3,8 @@ From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM Equivocation.
 From VLSM.Core Require Import Composition VLSMProjections Validator ProjectionTraces.
 
+Set Default Proof Using "Type".
+
 (** * VLSM projections and messages properties
 
   In this section we show that messages properties (oracles like [has_been_sent],
@@ -45,7 +47,7 @@ Lemma VLSM_projection_oracle_reflect
   (HstepwiseY : oracle_stepwise_props (vlsm := Y) selectorY oracleY)
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
   forall m, oracleY (state_project s) m -> oracleX s m.
-Proof.
+Proof using label_project Hsimul Hselector.
   intros s Hs m Hm.
   apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseX _ Hs m).
   intros isX trX HtrX.
@@ -74,7 +76,7 @@ Lemma VLSM_projection_has_been_sent_reflect
   `{HasBeenSentCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_sent Y (state_project s) m -> has_been_sent X s m.
-Proof.
+Proof using label_project Hsimul.
   apply VLSM_projection_oracle_reflect with (field_selector output) (field_selector output).
   - by intros [] [] **; cbn in *; subst.
   - by apply (has_been_sent_stepwise_props X).
@@ -86,7 +88,7 @@ Lemma VLSM_projection_has_been_received_reflect
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_received Y (state_project s) m -> has_been_received X s m.
-Proof.
+Proof using label_project Hsimul.
   apply VLSM_projection_oracle_reflect with (field_selector input) (field_selector input).
   - by intros [] [] **; cbn in *; subst.
   - by apply (has_been_received_stepwise_props X).
@@ -100,7 +102,7 @@ Lemma VLSM_projection_has_been_directly_observed_reflect
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_directly_observed Y (state_project s) m -> has_been_directly_observed X s m.
-Proof.
+Proof using label_project Hsimul.
   apply VLSM_projection_oracle_reflect with item_sends_or_receives item_sends_or_receives.
   - by intros [] [] **; cbn in *; subst.
   - by apply has_been_directly_observed_stepwise_props.
@@ -135,7 +137,7 @@ Lemma VLSM_weak_embedding_selected_message_exists_in_some_preloaded_traces
   s m
   : selected_message_exists_in_some_preloaded_traces X selectorX s m ->
   selected_message_exists_in_some_preloaded_traces Y selectorY (state_project s) m.
-Proof.
+Proof using label_project Hsimul Hselector.
   intros [is [tr [Htr Hm]]].
   destruct Htr as [Htr His].
   apply (VLSM_weak_embedding_finite_valid_trace_from_to Hsimul) in Htr.
@@ -163,7 +165,7 @@ Lemma VLSM_weak_embedding_oracle
   (HoracleY_dec : RelDecision oracleY)
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, oracleX s m -> oracleY (state_project s) m.
-Proof.
+Proof using label_project Hsimul Hselector.
   intros s Hs m Hm.
   apply (prove_all_have_message_from_stepwise _ _ _ _ HstepwiseX _ Hs m) in Hm.
   apply (selected_messages_consistency_prop_from_stepwise _ _ _ _ HstepwiseX HoracleX_dec _ Hs) in Hm.
@@ -180,7 +182,7 @@ Lemma VLSM_weak_embedding_has_been_sent
   `{HasBeenSentCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_sent X s m -> has_been_sent Y (state_project s) m.
-Proof.
+Proof using label_project Hsimul.
   apply VLSM_weak_embedding_oracle with (field_selector output) (field_selector output).
   - by intros [] [] Hin Hout; cbn in *; subst.
   - by apply (has_been_sent_stepwise_props X).
@@ -194,7 +196,7 @@ Lemma VLSM_weak_embedding_has_been_received
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_received X s m -> has_been_received Y (state_project s) m.
-Proof.
+Proof using label_project Hsimul.
   apply VLSM_weak_embedding_oracle with (field_selector input) (field_selector input).
   - by intros [] [] Hin Hout; cbn in *; subst.
   - by apply (has_been_received_stepwise_props X).
@@ -210,7 +212,7 @@ Lemma VLSM_weak_embedding_has_been_directly_observed
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_directly_observed X s m -> has_been_directly_observed Y (state_project s) m.
-Proof.
+Proof using label_project Hsimul.
   apply VLSM_weak_embedding_oracle with item_sends_or_receives item_sends_or_receives.
   - by intros [] [] **; cbn in *; subst.
   - by apply has_been_directly_observed_stepwise_props.
@@ -301,7 +303,7 @@ Lemma VLSM_incl_has_been_sent
   `{HasBeenSentCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_sent X s m -> has_been_sent Y s m.
-Proof.
+Proof using Hincl.
   intros s Hs m Hm.
   by eapply
     (@VLSM_embedding_has_been_sent _ X Y _ _
@@ -313,7 +315,7 @@ Lemma VLSM_incl_has_been_received
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_received X s m -> has_been_received Y s m.
-Proof.
+Proof using Hincl.
   intros s Hs m Hm.
   by eapply
     (@VLSM_embedding_has_been_received _ X Y _ _
@@ -327,7 +329,7 @@ Lemma VLSM_incl_has_been_directly_observed
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_directly_observed X s m -> has_been_directly_observed Y s m.
-Proof.
+Proof using Hincl.
   intros s Hs m Hm.
   by eapply
     (@VLSM_embedding_has_been_directly_observed _ X Y _ _
@@ -339,7 +341,7 @@ Lemma VLSM_incl_has_been_sent_reflect
   `{HasBeenSentCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_sent Y s m -> has_been_sent X s m.
-Proof.
+Proof using Hincl.
   intros s Hs m Hm.
   by eapply
     (@VLSM_embedding_has_been_sent_reflect _ X Y _ _
@@ -351,7 +353,7 @@ Lemma VLSM_incl_has_been_received_reflect
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_received Y s m -> has_been_received X s m.
-Proof.
+Proof using Hincl.
   intros s Hs m Hm.
   by eapply
     (@VLSM_embedding_has_been_received_reflect _ X Y _ _
@@ -365,7 +367,7 @@ Lemma VLSM_incl_has_been_directly_observed_reflect
   `{HasBeenReceivedCapability message Y}
   : forall s, valid_state_prop (pre_loaded_with_all_messages_vlsm X) s ->
     forall m, has_been_directly_observed Y s m -> has_been_directly_observed X s m.
-Proof.
+Proof using Hincl.
   intros s Hs m Hm.
   by eapply
     (@VLSM_embedding_has_been_directly_observed_reflect _ X Y _ _
@@ -393,7 +395,7 @@ Lemma same_IM_composite_has_been_sent_preservation s1 m
   (Hs1 : valid_state_prop (pre_loaded_with_all_messages_vlsm (free_composite_vlsm IM1)) s1)
   : composite_has_been_sent IM1 s1 m ->
     composite_has_been_sent IM2 (same_IM_state_rew Heq s1) m.
-Proof.
+Proof using H.
   specialize (same_IM_preloaded_free_embedding IM1 IM2 Heq) as Hproj.
   intros Hbs1_m.
   by specialize (VLSM_embedding_has_been_sent Hproj _ Hs1 m Hbs1_m).
@@ -424,7 +426,7 @@ Context
 *)
 Lemma can_emit_projection
   : can_emit PreFree m -> can_emit (pre_loaded_with_all_messages_vlsm (IM j)) m.
-Proof.
+Proof using validator sender Hsender_safety Hj A.
   destruct (sender m) as [v |] eqn: Hsender; simpl in Hj; [| by congruence].
   apply Some_inj in Hj.
   specialize (Hsender_safety _ _ Hsender).
diff --git a/theories/VLSM/Core/Equivocators/EquivocatorReplay.v b/theories/VLSM/Core/Equivocators/EquivocatorReplay.v
index 00127558..51e6906d 100644
--- a/theories/VLSM/Core/Equivocators/EquivocatorReplay.v
+++ b/theories/VLSM/Core/Equivocators/EquivocatorReplay.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections Equivocators.Equivocators.
 From VLSM.Core Require Import Equivocation EquivocationProjections Equivocators.MessageProperties.
 
+Set Default Proof Using "Type".
+
 (** * Equivocator State Append Determines a Projection
 
   In this module, we show that we can "append" two equivocator traces by
diff --git a/theories/VLSM/Core/Equivocators/Equivocators.v b/theories/VLSM/Core/Equivocators/Equivocators.v
index cca51c82..0221cfe0 100644
--- a/theories/VLSM/Core/Equivocators/Equivocators.v
+++ b/theories/VLSM/Core/Equivocators/Equivocators.v
@@ -4,6 +4,8 @@ From Coq Require Import Eqdep Fin FunctionalExtensionality.
 From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM VLSMProjections Composition.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocation
 
   An [equivocator_vlsm] for a given [VLSM] <<X>> is a VLSM which starts as a
diff --git a/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v b/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v
index 1031a513..722a11ba 100644
--- a/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v
+++ b/theories/VLSM/Core/Equivocators/EquivocatorsComposition.v
@@ -9,6 +9,8 @@ From VLSM.Core Require Import Equivocation.NoEquivocation.
 From VLSM.Core Require Import Equivocators.Equivocators.
 From VLSM.Core Require Import Equivocators.MessageProperties.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocator Composition
 
   Given a composition <<X>> of VLSMs, we can model equivocator behavior by
@@ -302,7 +304,7 @@ Definition not_equivocating_equivocator_descriptors
 
 #[export] Instance not_equivocating_equivocator_descriptors_dec
   : RelDecision not_equivocating_equivocator_descriptors.
-Proof.
+Proof using H.
   intros eqv_descriptors s.
   apply @Decision_iff with (P :=
     Forall (fun eqv => existing_descriptor (IM eqv) (eqv_descriptors eqv) (s eqv)) (enum index)).
diff --git a/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v b/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v
index 9986096b..1fd09c3a 100644
--- a/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v
+++ b/theories/VLSM/Core/Equivocators/EquivocatorsCompositionProjections.v
@@ -9,6 +9,8 @@ From VLSM.Core Require Import Equivocators.Equivocators Equivocators.Equivocator
 From VLSM.Core Require Import Equivocators.EquivocatorsComposition.
 From VLSM.Core Require Import Equivocators.MessageProperties.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocator Composition Projections *)
 
 Section sec_equivocators_composition_projections.
@@ -1516,7 +1518,7 @@ Qed.
 Lemma PreFreeE_PreFree_vlsm_partial_projection
   (final_descriptors : equivocator_descriptors)
   : VLSM_partial_projection PreFreeE PreFree (equivocators_partial_trace_project final_descriptors).
-Proof.
+Proof using equivocators_no_equivocations_vlsm H0.
   split; [by split; apply equivocators_partial_trace_project_extends_left |].
   intros s tr sX trX Hpr_tr Htr.
   destruct (destruct_equivocators_partial_trace_project Hpr_tr)
@@ -2105,7 +2107,7 @@ Lemma equivocators_valid_trace_from_project
     equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\
     equivocators_state_project final_descriptors final_state = final_stateX /\
     finite_valid_trace_from_to Free isX final_stateX trX.
-Proof.
+Proof using sub_IM H.
   apply valid_trace_get_last in Htr as Hfinal_state. apply valid_trace_forget_last in Htr.
   subst final_state.
   specialize (VLSM_partial_projection_finite_valid_trace_from
@@ -2152,7 +2154,7 @@ Qed.
 Lemma equivocators_no_equivocations_vlsm_X_vlsm_projection
   : VLSM_projection equivocators_no_equivocations_vlsm Free
       (equivocators_total_label_project IM) (equivocators_total_state_project IM).
-Proof.
+Proof using sub_IM H.
   constructor; [constructor |].
   - intros * Htr. apply PreFreeE_Free_vlsm_projection_type.
     apply VLSM_incl_finite_valid_trace_from; [| done].
@@ -2182,7 +2184,7 @@ Qed.
 Lemma preloaded_equivocators_no_equivocations_vlsm_X_vlsm_projection
   : VLSM_projection PreFreeE PreFree
       (equivocators_total_label_project IM) (equivocators_total_state_project IM).
-Proof.
+Proof using H0 H.
   constructor; [constructor; intros |].
   - by apply PreFreeE_Free_vlsm_projection_type.
   - intros * Htr.
diff --git a/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v b/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v
index a74f8418..b246bcec 100644
--- a/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v
+++ b/theories/VLSM/Core/Equivocators/EquivocatorsProjections.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
 From VLSM.Core Require Import VLSM VLSMProjections Equivocators.Equivocators.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Projecting Equivocator Traces *)
 
 Section sec_equivocator_vlsm_projections.
diff --git a/theories/VLSM/Core/Equivocators/FixedEquivocation.v b/theories/VLSM/Core/Equivocators/FixedEquivocation.v
index 14e28393..3e6c9d1e 100644
--- a/theories/VLSM/Core/Equivocators/FixedEquivocation.v
+++ b/theories/VLSM/Core/Equivocators/FixedEquivocation.v
@@ -10,6 +10,8 @@ From VLSM.Core Require Import Equivocators.MessageProperties.
 From VLSM.Core Require Import Equivocators.EquivocatorsComposition.
 From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocators Fixed Equivocation *)
 
 Section sec_equivocators_fixed_equivocations_vlsm.
@@ -252,7 +254,7 @@ Context
 (** The [full_node_constraint_alt] is stronger than the [fixed_equivocation_constraint]. *)
 Lemma fixed_equivocation_constraint_subsumption_alt
   : strong_constraint_subsumption IM full_node_constraint_alt fixed_equivocation_constraint.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   intros l (s, [m |]) Hc ; [| done].
   destruct Hc as [Hno_equiv | [i [Hi Hm]]]; [by left |].
   unfold node_generated_without_further_equivocation_alt in Hm.
@@ -270,7 +272,7 @@ Qed.
 Lemma fixed_equivocation_constraint_subsumption
   (Hno_resend : forall i : index, cannot_resend_message_stepwise_prop (IM i))
   : preloaded_constraint_subsumption IM full_node_constraint fixed_equivocation_constraint.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0 EqDecision0.
   intros l (s, om) Hv.
   apply fixed_equivocation_constraint_subsumption_alt.
   by eapply full_node_condition_for_admissible_equivocators_subsumption.
@@ -331,7 +333,7 @@ Lemma not_equivocating_equivocator_descriptors_proper_fixed
   (eqv_descriptors : equivocator_descriptors IM)
   (Heqv_descriptors : not_equivocating_equivocator_descriptors IM eqv_descriptors s)
   : proper_fixed_equivocator_descriptors eqv_descriptors s.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   apply not_equivocating_equivocator_descriptors_proper in Heqv_descriptors as Hproper.
   split; [done |].
   intros i Hi; rewrite <- elem_of_elements in Hi.
@@ -450,7 +452,7 @@ Lemma _equivocators_valid_trace_project
     equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\
     equivocators_state_project IM final_descriptors final_state = final_stateX /\
     finite_valid_trace X' isX trX.
-Proof.
+Proof using X H9 H6 H4 H3 H2 H1 H0.
   remember (length tr) as len_tr.
   revert tr Htr Heqlen_tr final_state final_descriptors Hproper.
   induction len_tr as [len_tr IHlen] using (well_founded_induction Wf_nat.lt_wf); intros.
@@ -618,7 +620,7 @@ Lemma free_equivocators_valid_trace_project
     equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\
     equivocators_state_project IM final_descriptors final_state = final_stateX /\
     finite_valid_trace (free_composite_vlsm IM) isX trX.
-Proof.
+Proof using X H9 H6 H4 H3 H2 H1 H0.
   by apply _equivocators_valid_trace_project.
 Qed.
 
@@ -639,7 +641,7 @@ Lemma not_equivocating_sent_message_has_been_directly_observed_in_projection
   (descriptors : equivocator_descriptors IM)
   (Hdescriptors : proper_fixed_equivocator_descriptors descriptors lst)
   : has_been_directly_observed Free (equivocators_state_project IM descriptors lst) m.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   destruct (free_equivocators_valid_trace_project descriptors is tr Hdescriptors Htr)
     as [trX [initial_descriptors [_ [Htr_project [Hfinal_state HtrX_Free]]]]].
   subst lst.
@@ -767,7 +769,7 @@ Lemma equivocators_trace_sub_item_input_is_seeded_or_sub_previously_sent
   : trace_sub_item_input_is_seeded_or_sub_previously_sent
     (equivocator_IM IM) (elements equivocating)
     (composite_has_been_directly_observed IM lst_trX) tr.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   intros pre item suf m Heq Hm Hitem.
   destruct (free_equivocators_valid_trace_project descriptors is tr Hproper Htr)
     as [trX [initial_descriptors [Hinitial_descriptors [Htr_project [Hfinal_state HtrXFree]]]]].
@@ -912,7 +914,7 @@ Lemma equivocator_vlsm_trace_project_reflect_non_equivocating
   (Houtput : output item = Some m)
   (Hno_equiv_item : projT1 (l item) ∉ equivocating)
   : trace_has_message (field_selector output) m trX.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   apply elem_of_list_split in Hitem.
   destruct Hitem as [pre [suf Heq_tr]].
   change (item :: suf) with ([item] ++ suf) in Heq_tr.
@@ -984,7 +986,7 @@ Lemma projection_has_not_been_directly_observed_is_equivocating
   (Hno : ~ composite_has_been_directly_observed IM sX m)
   : forall item : composite_transition_item (equivocator_IM IM),
       item ∈ tr -> output item = Some m -> projT1 (l item) ∈ equivocating.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   destruct (free_equivocators_valid_trace_project descriptors is tr Hproper Htr)
     as [trX [initial_descriptors [_ [Htr_project [Hlast_state HtrX]]]]].
   intros item Hitem Houtput.
@@ -1117,7 +1119,7 @@ Qed.
 Lemma fixed_equivocation_constraint_has_constraint_has_been_sent_prop
   : constraint_has_been_sent_prop
     (fixed_equivocation_constraint IM equivocating).
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   unfold constraint_has_been_sent_prop. intros.
   remember (equivocators_state_project _ _ _) as sX.
   destruct (composite_has_been_directly_observed_dec IM sX m)
@@ -1296,7 +1298,7 @@ Theorem fixed_equivocators_valid_trace_project
     equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\
     equivocators_state_project IM final_descriptors final_state = final_stateX /\
     finite_valid_trace X isX trX.
-Proof.
+Proof using H6 H4 H3 H2 H1 H0.
   apply _equivocators_valid_trace_project; [done | done | done |]; intros.
   by apply fixed_equivocation_constraint_has_constraint_has_been_sent_prop.
 Qed.
@@ -1304,7 +1306,7 @@ Qed.
 Lemma fixed_equivocators_vlsm_partial_projection
   (final_descriptors : equivocator_descriptors IM)
   : VLSM_partial_projection XE X (equivocators_partial_trace_project IM final_descriptors).
-Proof.
+Proof using H6 H4 H3 H2 H1 H0 H.
   split; [split |].
   - intros s tr sX trX Hpr_tr s_pre pre Hs_lst Hpre_tr.
     assert (HPreFree_pre_tr :
@@ -1330,7 +1332,7 @@ Qed.
 
 Lemma fixed_equivocators_vlsm_projection
   : VLSM_projection XE X (equivocators_total_label_project IM) (equivocators_total_state_project IM).
-Proof.
+Proof using H6 H4 H3 H2 H1 H0 H.
   constructor; [constructor |]; intros sX trX HtrX.
   - apply PreFreeE_Free_vlsm_projection_type.
     apply VLSM_incl_finite_valid_trace_from; [| done].
diff --git a/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v b/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v
index 09357d3e..1a002552 100644
--- a/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v
+++ b/theories/VLSM/Core/Equivocators/FixedEquivocationSimulation.v
@@ -12,6 +12,8 @@ From VLSM.Core Require Import Equivocators.FullReplayTraces.
 From VLSM.Core Require Import Equivocators.FixedEquivocation.
 From VLSM.Core Require Import Equivocators.SimulatingFree.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocators Simulating fixed-set equivocation composition
 
   In this module we show that the composition of equivocators with no
@@ -46,7 +48,7 @@ Context {message : Type}
 
 Lemma no_initial_messages_in_sub_IM
   : forall i m, ~ vinitial_message_prop (sub_IM IM (elements equivocating) i) m.
-Proof.
+Proof using no_initial_messages_in_IM.
   intros [i Hi] m Hinit.
   by apply (no_initial_messages_in_IM i m).
 Qed.
@@ -156,7 +158,7 @@ Lemma fixed_equivocation_replay_has_message
     s im)
   : composite_has_been_sent (equivocator_IM IM)
       (lift_equivocators_sub_state_to IM (elements equivocating) eqv_state_s s) im.
-Proof.
+Proof using H7.
   apply non_empty_valid_trace_from_can_produce in Him
      as (im_eis & im_etr & item & Him_etr & Hlast & Heqs & Him).
   specialize
@@ -190,7 +192,8 @@ Lemma fixed_equivocation_has_replayable_message_prop
   : replayable_message_prop IM (fun _ : message => False)
     (strong_fixed_equivocation_constraint IM equivocating)
     (equivocators_fixed_equivocations_constraint IM (elements equivocating)).
-Proof.
+Proof using Ci EqDecision0 Free FreeE H5 H7 H8 IM PreFreeE SubFreeE X XE
+equivocating index message no_initial_messages_in_IM.
   specialize (vlsm_is_pre_loaded_with_False XE) as HeqXE.
   specialize (vlsm_is_pre_loaded_with_False X) as HeqX.
   specialize (equivocators_fixed_equivocations_vlsm_incl_PreFree IM (elements equivocating)) as HinclE.
@@ -269,8 +272,7 @@ Proof.
     { by apply (VLSM_eq_valid_state HeqXE), (VLSM_eq_valid_state HeqXE). }
     spec Hreplay.
     { subst s.
-      clear -HeqXE Hstate_valid.
-      intros l s om Hv Hlift_s.
+      intros l' s om Hv Hlift_s.
       apply (VLSM_eq_valid_state HeqXE) in Hstate_valid.
       apply (VLSM_eq_valid_state HeqXE) in Hlift_s.
       by apply fixed_equivocating_non_equivocating_constraint_lifting.
@@ -338,7 +340,7 @@ Lemma fixed_equivocators_finite_valid_trace_init_to_rev
       equivocators_total_trace_project IM tr = trX /\
       finite_valid_trace_init_to XE is s tr /\
       finite_trace_last_output trX = finite_trace_last_output tr.
-Proof.
+Proof using Ci EqDecision0 Free FreeE H5 H7 H8 IM PreFreeE SubFreeE X XE equivocating index message no_initial_messages_in_IM.
   (*
     Since the base result works with pre-loaded vlsms, some massaging of the
     hypothesis and conclusion is done to fit the applied lemma.
diff --git a/theories/VLSM/Core/Equivocators/FullReplayTraces.v b/theories/VLSM/Core/Equivocators/FullReplayTraces.v
index 3537453a..37e66997 100644
--- a/theories/VLSM/Core/Equivocators/FullReplayTraces.v
+++ b/theories/VLSM/Core/Equivocators/FullReplayTraces.v
@@ -9,6 +9,8 @@ From VLSM.Core Require Import Equivocators.EquivocatorReplay Equivocators.Messag
 From VLSM.Core Require Import Equivocators.EquivocatorsComposition.
 From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections Plans.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocator Full Replay Traces
 
   In this section we show that given a trace of equivocators, one can "replay"
@@ -503,7 +505,7 @@ Lemma replayed_initial_state_from_valid
   (His : composite_initial_state_prop sub_equivocator_IM is)
   : finite_valid_trace_from SeededCE full_replay_state
       (replayed_initial_state_from full_replay_state is).
-Proof.
+Proof using Hfull_replay_state Hconstraint_none.
   cut (forall l, incl l (enum (sub_index equivocating)) ->
     finite_valid_plan_from SeededCE
       full_replay_state (map (initial_new_machine_transition_item is) l)).
@@ -532,7 +534,7 @@ Qed.
 
 Lemma lift_initial_message
   : forall m, vinitial_message_prop SeededXE m -> valid_message_prop SeededCE m.
-Proof.
+Proof using Hseed.
   intros m [Hinit | Hseeded].
   - apply initial_message_is_valid. destruct Hinit as [[i Hi] Hinit].
     by left; exists i.
@@ -543,7 +545,7 @@ Lemma lift_equivocators_sub_weak_projection :
   VLSM_weak_embedding SeededXE SeededCE
     (lift_equivocators_sub_label_to full_replay_state)
     (lift_equivocators_sub_state_to full_replay_state).
-Proof.
+Proof using Hsubsumption Hseed Hfull_replay_state Hconstraint_none.
   apply basic_VLSM_weak_embedding; intros ? *.
   - split.
     + by apply lift_equivocators_sub_valid, Hv.
@@ -560,7 +562,7 @@ Lemma sub_preloaded_replayed_trace_from_valid_equivocating
   (Htr : finite_valid_trace SeededXE is tr)
   : finite_valid_trace_from SeededCE
       full_replay_state (replayed_trace_from full_replay_state is tr).
-Proof.
+Proof using Hsubsumption Hseed Hfull_replay_state Hconstraint_none.
   destruct Htr as [Htr His].
   apply finite_valid_trace_from_app_iff.
   split; [by apply replayed_initial_state_from_valid |].
@@ -622,7 +624,7 @@ Context
       equivocator_IM (free_constraint _) seed
       (lift_equivocators_sub_label_to full_replay_state l)
       (lift_equivocators_sub_state_to full_replay_state s, om).
-Proof.
+Proof using Hfull_replay_state.
   intros l s om (Hs & _ & _ & Hc1 & _).
   split; [| done].
   destruct om as [m |]; [| done].
@@ -666,7 +668,7 @@ Lemma SeededXE_SeededNoEquiv_weak_embedding :
   VLSM_weak_embedding SeededXE SeededAllXE
     (lift_equivocators_sub_label_to full_replay_state)
     (lift_equivocators_sub_state_to full_replay_state).
-Proof.
+Proof using Hfull_replay_state.
   constructor.
   apply lift_equivocators_sub_weak_projection; intros; [done | | done |].
   - by apply sent_are_valid.
@@ -679,7 +681,7 @@ Lemma sub_replayed_trace_from_valid_equivocating
   (Htr : finite_valid_trace SeededXE is tr)
   : finite_valid_trace_from SeededAllXE
       full_replay_state (replayed_trace_from full_replay_state is tr).
-Proof.
+Proof using Hfull_replay_state.
   unfold composite_no_equivocation_vlsm_with_pre_loaded in SeededAllXE.
   specialize (sub_preloaded_replayed_trace_from_valid_equivocating
     (no_equivocations_additional_constraint_with_pre_loaded equivocator_IM (free_constraint _) seed)
diff --git a/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v b/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v
index 2cdf71c9..8c3c7d55 100644
--- a/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v
+++ b/theories/VLSM/Core/Equivocators/LimitedEquivocationSimulation.v
@@ -16,6 +16,8 @@ From VLSM.Core Require Import
   Equivocators.FixedEquivocationSimulation.
 From VLSM.Core Require Import Equivocators.FixedEquivocation.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Equivocators Simulating limited message equivocation traces
 
   In this module we show that the composition of equivocators with no-message
@@ -139,7 +141,7 @@ Lemma equivocators_limited_valid_trace_projects_to_annotated_limited_equivocatio
             Datatypes.id original_state trX /\
       finite_valid_trace_init_to XE is s tr /\
       finite_trace_last_output trX = finite_trace_last_output tr.
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Hchannel H19 H18 H16 H15 H11 FullMessageDependencies0 EqDecision1.
   apply valid_trace_get_last in HtrX as HeqsX.
   eapply valid_trace_forget_last, @msg_dep_fixed_limited_equivocation in HtrX; [| done..].
   apply limited_equivocators_finite_valid_trace_init_to_rev in HtrX
diff --git a/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v b/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v
index 3bc95528..e05d2e98 100644
--- a/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v
+++ b/theories/VLSM/Core/Equivocators/LimitedStateEquivocation.v
@@ -12,6 +12,8 @@ From VLSM.Core Require Import Equivocators.EquivocatorsComposition.
 From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections.
 From VLSM.Core Require Import Equivocators.FixedEquivocation.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Limited Equivocation *)
 Definition composite_constraint
   {index message} (IM : index -> VLSM message) : Type :=
@@ -283,7 +285,7 @@ Lemma equivocators_limited_valid_trace_projects_to_annotated_limited_equivocatio
     finite_valid_trace (msg_dep_limited_equivocation_vlsm IM threshold full_message_dependencies sender (Cv := Ci))
       {| original_state := isX; state_annotation := ` inhabitant |}
       (msg_dep_annotate_trace_with_equivocators IM full_message_dependencies sender isX trX).
-Proof.
+Proof using no_initial_messages_in_IM message_dependencies Hchannel HMsgDep HFullMsgDep H18 H16 H15 H11 EqDecision1.
   eapply equivocators_limited_valid_trace_projects_to_fixed_limited_equivocation
       in Htr as (trX & initial_descriptors & Hinitial_descriptors & Hpr & Hlst_pr & Hpr_limited)
   ; [| done].
@@ -328,7 +330,7 @@ Lemma limited_equivocators_valid_trace_project
     equivocators_trace_project IM final_descriptors tr = Some (trX, initial_descriptors) /\
     equivocators_state_project final_descriptors final_state = final_stateX /\
     finite_valid_trace Limited isX trX.
-Proof.
+Proof using Hsender_safety H0.
   specialize
     (equivocators_limited_valid_trace_projects_to_fixed_limited_equivocation
       final_descriptors is tr Hproper Htr)
@@ -348,7 +350,7 @@ Lemma limited_equivocators_vlsm_partial_projection
   (final_descriptors : equivocator_descriptors)
   : VLSM_partial_projection equivocators_limited_equivocations_vlsm Limited
       (equivocators_partial_trace_project IM final_descriptors).
-Proof.
+Proof using Hsender_safety H0.
   split; [split |].
   - intros s tr sX trX Hpr_tr s_pre pre Hs_lst Hpre_tr.
     assert (HPreFree_pre_tr :
@@ -377,7 +379,7 @@ Qed.
 Lemma limited_equivocators_vlsm_projection
   : VLSM_projection equivocators_limited_equivocations_vlsm Limited
     (equivocators_total_label_project IM) (equivocators_total_state_project IM).
-Proof.
+Proof using Hsender_safety H0.
   constructor; [constructor |]; intros ? *.
   - intros HtrX. apply PreFreeE_Free_vlsm_projection_type.
     revert HtrX. apply VLSM_incl_finite_valid_trace_from.
diff --git a/theories/VLSM/Core/Equivocators/MessageProperties.v b/theories/VLSM/Core/Equivocators/MessageProperties.v
index 0c69ab34..a96710ef 100644
--- a/theories/VLSM/Core/Equivocators/MessageProperties.v
+++ b/theories/VLSM/Core/Equivocators/MessageProperties.v
@@ -5,6 +5,8 @@ From VLSM.Lib Require Import ListSetExtras FinExtras.
 From VLSM.Core Require Import VLSM Equivocation.
 From VLSM.Core Require Import Equivocators.Equivocators Equivocators.EquivocatorsProjections.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Message Properties *)
 
 Section sec_equivocator_vlsm_message_properties.
@@ -259,7 +261,7 @@ Definition equivocator_oracle
 
 Lemma equivocator_oracle_dec
   : RelDecision equivocator_oracle.
-Proof.
+Proof using Hdec.
   intros s m.
   eapply
     (Decision_iff
@@ -279,7 +281,7 @@ Qed.
 
 Lemma equivocator_oracle_stepwise_props
   : oracle_stepwise_props (vlsm := equivocator_vlsm) equivocator_selector equivocator_oracle.
-Proof.
+Proof using Hstepwise Hselector_io.
   destruct Hstepwise.
   split; intros.
   - destruct H as [Hn His]. unfold is_singleton_state in Hn.
@@ -543,7 +545,7 @@ Qed.
 
 Lemma equivocator_ComputableSentMessages :
   ComputableSentMessages equivocator_vlsm.
-Proof.
+Proof using EqDecision0 ComputableSentMessages0.
   constructor 1 with equivocator_sent_messages_set; constructor; intros.
   - rewrite <- equivocator_elem_of_sent_messages_set.
     by eapply equivocator_has_been_sent_stepwise_props.
diff --git a/theories/VLSM/Core/Equivocators/SimulatingFree.v b/theories/VLSM/Core/Equivocators/SimulatingFree.v
index d4157a13..c755f549 100644
--- a/theories/VLSM/Core/Equivocators/SimulatingFree.v
+++ b/theories/VLSM/Core/Equivocators/SimulatingFree.v
@@ -8,6 +8,8 @@ From VLSM.Core Require Import Equivocators.EquivocatorsComposition.
 From VLSM.Core Require Import Equivocators.EquivocatorsCompositionProjections.
 From VLSM.Core Require Import Equivocators.FullReplayTraces.
 
+Set Default Proof Using "Type".
+
 (** * Equivocators simulating regular nodes
 
   In this module we prove a general simulation result parameterized by
@@ -110,7 +112,7 @@ Lemma generalized_equivocators_finite_valid_trace_init_to_rev
     exists tr, equivocators_total_trace_project IM tr = trX /\
     finite_valid_trace_init_to CE is s tr /\
     finite_trace_last_output trX = finite_trace_last_output tr.
-Proof.
+Proof using H.
   assert (HinclE : VLSM_incl CE PreFreeE)
     by apply composite_pre_loaded_vlsm_incl_pre_loaded_with_all_messages.
   induction HtrX using finite_valid_trace_init_to_rev_strong_ind.
@@ -312,7 +314,7 @@ Lemma seeded_equivocators_finite_valid_trace_init_to_rev
     exists tr, equivocators_total_trace_project IM tr = trX /\
     finite_valid_trace_init_to SeededXE is s tr /\
     finite_trace_last_output trX = finite_trace_last_output tr.
-Proof.
+Proof using H.
   apply
     (generalized_equivocators_finite_valid_trace_init_to_rev IM)
   ; [.. | done].
@@ -391,7 +393,7 @@ Lemma equivocators_finite_valid_trace_init_to_rev
     exists tr, equivocators_total_trace_project IM tr = trX /\
     finite_valid_trace_init_to XE is s tr /\
     finite_trace_last_output trX = finite_trace_last_output tr.
-Proof.
+Proof using H.
   specialize (vlsm_is_pre_loaded_with_False Free) as Heq.
   apply (VLSM_eq_finite_valid_trace_init_to Heq) in HtrX.
   specialize
diff --git a/theories/VLSM/Core/MessageDependencies.v b/theories/VLSM/Core/MessageDependencies.v
index 256b2bdc..03db6f4b 100644
--- a/theories/VLSM/Core/MessageDependencies.v
+++ b/theories/VLSM/Core/MessageDependencies.v
@@ -4,6 +4,8 @@ From VLSM.Lib Require Import Preamble ListExtras ListFinSetExtras.
 From VLSM.Core Require Import VLSM VLSMProjections Composition ProjectionTraces.
 From VLSM.Core Require Import SubProjectionTraces Equivocation EquivocationProjections.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Message Dependencies
 
   An abstract framework for the full-node condition.
@@ -133,7 +135,7 @@ Lemma msg_dep_reflects_validity
   : forall dm m, msg_dep_rel dm m ->
     valid_message_prop (pre_loaded_vlsm X P) m ->
     valid_message_prop (pre_loaded_vlsm X P) dm.
-Proof.
+Proof using MessageDependencies0 Irreflexive0 HasBeenSentCapability0 HasBeenReceivedCapability0.
   intros dm m Hdm.
   rewrite emitted_messages_are_valid_iff, can_emit_iff.
   intros [Hinit | [s Hproduce]].
@@ -165,7 +167,7 @@ Lemma msg_dep_has_been_sent
   m
   (Hsent : has_been_sent X s m)
   : forall dm, msg_dep_rel dm m -> has_been_directly_observed X s dm.
-Proof.
+Proof using MessageDependencies0 Irreflexive0.
   revert m Hsent; induction Hs using valid_state_prop_ind; intro m.
   - intro Hbs; contradict Hbs.
     by apply has_been_sent_no_inits.
@@ -216,7 +218,7 @@ Lemma msg_dep_full_node_reflects_has_been_directly_observed
   (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm X) s)
   : forall dm m, msg_dep_rel dm m ->
     has_been_directly_observed X s m -> has_been_directly_observed X s dm.
-Proof.
+Proof using MessageDependencies0 Irreflexive0.
   intros dm m Hdm [Hsent | Hreceived].
   - by eapply msg_dep_has_been_sent.
   - by eapply full_node_has_been_received.
@@ -232,7 +234,7 @@ Lemma msg_dep_full_node_happens_before_reflects_has_been_directly_observed
   (Hs : valid_state_prop (pre_loaded_with_all_messages_vlsm X) s)
   : forall dm m, msg_dep_happens_before dm m ->
     has_been_directly_observed X s m -> has_been_directly_observed X s dm.
-Proof.
+Proof using MessageDependencies0 Irreflexive0.
   intros dm m Hdm Hobs.
   eapply msg_dep_happens_before_reflect; [| done ..].
   by apply msg_dep_full_node_reflects_has_been_directly_observed.
@@ -248,7 +250,7 @@ Lemma msg_dep_full_node_input_valid_happens_before_has_been_directly_observed
   (Hvalid : input_valid (pre_loaded_with_all_messages_vlsm X) l (s, Some m))
   : forall dm, msg_dep_happens_before dm m ->
     has_been_directly_observed X s dm.
-Proof.
+Proof using MessageDependencies0 Irreflexive0.
   intro dm; rewrite msg_dep_happens_before_iff_one; intros [Hdm | (dm' & Hdm' & Hdm)].
   - by eapply Hfull; [apply Hvalid |].
   - eapply msg_dep_happens_before_reflect; [| done |].
@@ -514,7 +516,7 @@ Context
 *)
 #[export] Instance composite_message_dependencies
   : MessageDependencies (free_composite_vlsm IM) message_dependencies.
-Proof.
+Proof using H10.
   split.
   - intros m s' ((s, iom) & [i li] & Ht) dm Hdm.
     apply composite_has_been_directly_observed_free_iff.
@@ -533,7 +535,7 @@ Lemma msg_dep_reflects_free_validity
   (X := free_composite_vlsm IM)
   : forall dm m, msg_dep_rel message_dependencies dm m ->
     valid_message_prop X m -> valid_message_prop X dm.
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H10.
   intros dm m Hdm.
   rewrite !emitted_messages_are_valid_iff.
   intros [[i [[im Him] _]] | Hemit]
@@ -563,7 +565,7 @@ Lemma msg_dep_reflects_happens_before_free_validity
   (X := free_composite_vlsm IM)
   : forall dm m, msg_dep_happens_before message_dependencies dm m ->
     valid_message_prop X m -> valid_message_prop X dm.
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H10.
   by apply msg_dep_happens_before_reflect, msg_dep_reflects_free_validity.
 Qed.
 
@@ -578,7 +580,7 @@ Lemma msg_dep_happens_before_composite_no_initial_valid_messages_emitted_by_send
     forall dm, msg_dep_happens_before message_dependencies dm m ->
     exists v, sender dm = Some v /\
       can_emit (pre_loaded_with_all_messages_vlsm (IM (A v))) dm.
-Proof.
+Proof using Irreflexive0 H9 H8 H7 H10.
   intros m Hm dm Hdm.
   cut (valid_message_prop X dm).
   - by apply composite_no_initial_valid_messages_emitted_by_sender.
@@ -778,7 +780,7 @@ Lemma tc_composite_observed_before_send_subsumes_happens_before
   forall m, can_emit Free m ->
   forall dm, msg_dep_happens_before message_dependencies dm m ->
     tc_composite_observed_before_send dm m.
-Proof.
+Proof using H7.
   intros m Hm dm Hdm.
   induction Hdm; [by eapply tc_composite_observed_before_send_subsumes_msg_dep_rel |].
   transitivity y; [| by apply IHHdm].
@@ -829,7 +831,7 @@ Definition full_node_is_globally_equivocating
 Lemma full_node_is_globally_equivocating_stronger s v :
   full_node_is_globally_equivocating s v ->
   msg_dep_is_globally_equivocating s v.
-Proof.
+Proof using EqDecision1.
   intros [m []]; exists m; constructor; [done | | done].
   by constructor 1; apply composite_has_been_directly_observed_sent_received_iff; right.
 Qed.
@@ -923,7 +925,7 @@ Lemma msg_dep_reflects_sub_free_validity
   : forall dm m, msg_dep_rel message_dependencies dm m ->
     valid_message_prop (pre_loaded_vlsm X P) m ->
     valid_message_prop (pre_loaded_vlsm X P) dm.
-Proof.
+Proof using Irreflexive0 H17 H16 H15.
   eapply msg_dep_reflects_validity; [| | done].
   - by typeclasses eauto.
   - intros m [sub_i [[im Him] Heqm]].
@@ -969,7 +971,7 @@ Context
 
 #[export] Instance msg_dep_happens_before_dec :
  RelDecision (msg_dep_happens_before message_dependencies).
-Proof.
+Proof using full_message_dependencies HFullMsgDep.
  refine
    (fun m1 m2 =>
       match decide (m1 ∈ full_message_dependencies m2) with
@@ -982,7 +984,7 @@ Qed.
 
 #[export] Instance msg_dep_happens_before_irrefl :
   Irreflexive (msg_dep_happens_before message_dependencies).
-Proof.
+Proof using full_message_dependencies HFullMsgDep.
   intros m Hm.
   contradict Hm.
   rewrite <- full_message_dependencies_happens_before.
@@ -995,7 +997,7 @@ Qed.
 Lemma msg_dep_rel_full_message_dependecies_subset :
   forall x y : message, msg_dep_rel message_dependencies x y ->
     full_message_dependencies x ⊆ full_message_dependencies y.
-Proof.
+Proof using HFullMsgDep.
   intros; intros z Hz.
   apply full_message_dependencies_happens_before.
   transitivity x; [by apply full_message_dependencies_happens_before |].
@@ -1003,7 +1005,7 @@ Proof.
 Qed.
 
 Lemma msg_dep_happens_before_wf : well_founded (msg_dep_happens_before message_dependencies).
-Proof.
+Proof using full_message_dependencies HFullMsgDep.
   apply tc_wf_projected with (<) (fun m => length (elements (full_message_dependencies m)));
     [by typeclasses eauto | | by apply Wf_nat.lt_wf].
   intros; unfold lt.
@@ -1023,7 +1025,7 @@ Lemma FullMessageDependencies_ind
   (IHm : forall dm, dm ∈ full_message_dependencies m ->
     (forall dm0, dm0 ∈ full_message_dependencies dm -> P dm0) -> P dm)
   : forall dm, dm ∈ full_message_dependencies m -> P dm.
-Proof.
+Proof using message_dependencies HFullMsgDep H6 H5 H4 H3 H2 H1 H0 EqDecision0.
   induction m  as (m & Hm) using (well_founded_ind msg_dep_happens_before_wf).
   intros dm Hdm.
   apply IHm; [done |].
@@ -1111,7 +1113,7 @@ Lemma free_valid_from_valid_dependencies
     forall dm, dm ∈ full_message_dependencies m ->
       valid_message_prop (free_composite_vlsm IM) dm)
   : valid_message_prop (free_composite_vlsm IM) m.
-Proof.
+Proof using H9 H8 H7 H6 H5 H4 H3 H10 EqDecision1.
   eapply emitted_messages_are_valid, free_valid_preloaded_lifts_can_be_emitted; [| done].
   by intros; apply Hdeps, full_message_dependencies_happens_before, msg_dep_happens_before_iff_one;
     left.
@@ -1125,7 +1127,7 @@ Lemma free_valid_from_all_dependencies_emitable_from_dependencies :
   forall m,
     all_dependencies_emittable_from_dependencies_prop m ->
       valid_message_prop (free_composite_vlsm IM) m.
-Proof.
+Proof using H9 H7 H6 H5 H4 H3 H10 EqDecision1.
   intros m Hm.
   specialize (Hm m) as Hemit; spec Hemit; [left |].
   inversion Hemit as [v _ Hemit']; clear Hemit.
@@ -1147,7 +1149,7 @@ Qed.
 Lemma valid_free_validating_is_message_validating
   : forall i, valid_all_dependencies_emittable_from_dependencies_prop i ->
     component_message_validator_prop IM (free_constraint IM) i.
-Proof.
+Proof using H9 H7 H6 H5 H4 H3 H10 EqDecision1.
   by intros i Hvalidating l s im Hv
   ; eapply free_valid_from_all_dependencies_emitable_from_dependencies, Hvalidating.
 Qed.
@@ -1165,7 +1167,7 @@ Lemma valid_free_validating_equiv_message_validating
   (no_initial_messages_in_IM : no_initial_messages_in_IM_prop IM)
   : forall i, component_message_validator_prop IM (free_constraint IM) i <->
   valid_all_dependencies_emittable_from_dependencies_prop i.
-Proof.
+Proof using H.
   intros i; split; [| apply valid_free_validating_is_message_validating].
   intros Hvalidator l s m Hv dm Hdm.
   specialize (Hvalidator l s m Hv).
@@ -1197,7 +1199,7 @@ Context
 #[export] Instance CompositeHasBeenObserved_dec
   `{FullMessageDependencies message Cm message_dependencies full_message_dependencies}
   : RelDecision (CompositeHasBeenObserved IM message_dependencies).
-Proof.
+Proof using H7 EqDecision1.
   intros s m.
   destruct (decide (composite_has_been_directly_observed IM s m));
     [by left; constructor |].
@@ -1245,7 +1247,7 @@ Lemma input_valid_transition_preserves_msg_dep_is_globally_equivocating :
     forall v, A v = j ->
       msg_dep_is_globally_equivocating IM message_dependencies sender s v ->
       msg_dep_is_globally_equivocating IM message_dependencies sender (destination item) v.
-Proof.
+Proof using Hsender_safety Hauth.
   intros s item Ht j Hsj v Hv [m []].
   exists m; constructor; [done | ..].
   - by eapply transition_preserves_CompositeHasBeenObserved.
diff --git a/theories/VLSM/Core/Plans.v b/theories/VLSM/Core/Plans.v
index 1c49cc76..dc33bd24 100644
--- a/theories/VLSM/Core/Plans.v
+++ b/theories/VLSM/Core/Plans.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Plans *)
 
 Section sec_plans.
diff --git a/theories/VLSM/Core/ProjectionTraces.v b/theories/VLSM/Core/ProjectionTraces.v
index 36bd196c..225ce90a 100644
--- a/theories/VLSM/Core/ProjectionTraces.v
+++ b/theories/VLSM/Core/ProjectionTraces.v
@@ -3,6 +3,8 @@ From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble StdppExtras.
 From VLSM.Core Require Import VLSM Composition VLSMProjections Validator.
 
+Set Default Proof Using "Type".
+
 Section sec_projections.
 
 (** * Composite VLSM induced projections
diff --git a/theories/VLSM/Core/ReachableThreshold.v b/theories/VLSM/Core/ReachableThreshold.v
index d9834458..6fb5b12d 100644
--- a/theories/VLSM/Core/ReachableThreshold.v
+++ b/theories/VLSM/Core/ReachableThreshold.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From Coq Require Import Reals Lra.
 From VLSM.Lib Require Import RealsExtras Measurable ListExtras StdppListSet.
 
+Set Default Proof Using "Type".
+
 (**
   Given a set of validators and a [threshold] (a positive real number), we say
   that the threshold is reachable ([rt_reachable]) when there exists a
@@ -73,7 +75,7 @@ Lemma pivotal_validator_extension
   exists v,
     v ∈ vs /\
     (sum_weights (vs ∖ {[ v ]} ∪ vsfix) <= threshold)%R.
-Proof.
+Proof using H6 H3 H0 EqDecision0.
   intros vsfix vss Hvsfix Hdisj Hall.
   destruct (pivotal_validator_extension_list (elements vsfix) (elements vss))
     as (vs & Hnd_vs & Hincl & Hvs & v & Hv & Hvs_v);
@@ -123,7 +125,7 @@ Lemma validators_pivotal_ind
   exists v,
     v ∈ vs /\
     (sum_weights (vs ∖ {[ v ]}) <= threshold)%R.
-Proof.
+Proof using Hrt H6 H3 H2 H0 EqDecision0.
   intros vss Hvss.
   destruct (pivotal_validator_extension ∅ vss)
     as (vs & Hincl & Hvs & v & Hv & Hvs').
@@ -146,7 +148,7 @@ Lemma sufficient_validators_pivotal
     exists v,
       v ∈ vs /\
       (sum_weights (vs ∖ {[ v ]}) <= threshold)%R.
-Proof.
+Proof using Hrt H6 H3 H2 H0 EqDecision0.
   destruct (rt_reachable (1 := Hrt)) as [vs Hweight].
   apply (validators_pivotal_ind vs) in Hweight as (vs' & Hincl & Hvs').
   by exists vs'.
@@ -169,7 +171,7 @@ Definition potentially_pivotal (v : V) : Prop :=
 *)
 Lemma exists_pivotal_validator :
   exists v, potentially_pivotal v.
-Proof.
+Proof using Hrt H6 H4 H3 H2 H1 H0 EqDecision0.
   destruct sufficient_validators_pivotal as (vs & Hgt & v & Hin & Hlte).
   exists v, (vs ∖ {[ v ]}); split_and!.
   - by rewrite elem_of_difference, elem_of_singleton; intros [].
diff --git a/theories/VLSM/Core/SubProjectionTraces.v b/theories/VLSM/Core/SubProjectionTraces.v
index 9ac57af5..a259ed4f 100644
--- a/theories/VLSM/Core/SubProjectionTraces.v
+++ b/theories/VLSM/Core/SubProjectionTraces.v
@@ -5,6 +5,8 @@ From VLSM.Lib Require Import Preamble ListExtras StdppListSet StdppExtras StdppL
 From VLSM.Core Require Import VLSM VLSMProjections ProjectionTraces Composition Validator.
 From VLSM.Core Require Import Equivocation EquivocationProjections Equivocation.NoEquivocation.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Subcomposition *)
 
 Section sec_sub_composition.
@@ -603,11 +605,10 @@ Proof.
     + unfold pre_VLSM_projection_transition_item_project in HitemX.
       destruct (composite_label_sub_projection_option _); [| by congruence].
       by inversion HitemX.
-  - clear -Hmsg Sub_Free Hlst His IHtr.
-    destruct iom as [m |]; [| done].
+  - destruct iom as [m |]; [| done].
     simpl in *.
     remember {| input := Some m |} as x.
-    assert (Hx : from_sub_projection x).
+    assert (Hx' : from_sub_projection x).
     {
       unfold from_sub_projection at 1, pre_VLSM_projection_in_projection,
         composite_label_sub_projection_option.
@@ -914,7 +915,7 @@ Qed.
 Lemma preloaded_lift_sub_state_to_initial_state :
   weak_projection_initial_state_preservation PreSubFree PreFree
     (lift_sub_state_to IM equivocators base_s).
-Proof.
+Proof using EqDecision0 Free Hbase_s IM PreFree PreSubFree SubFree base_s equivocating_IM equivocators index message.
   apply valid_state_has_trace in Hbase_s as Htr.
   destruct Htr as [is [tr Htr]].
   intros eqv_is Heqv_is.
@@ -963,7 +964,7 @@ Qed.
 Lemma PreSubFree_PreFree_weak_embedding :
   VLSM_weak_embedding PreSubFree PreFree
     (lift_sub_label IM equivocators) (lift_sub_state_to IM equivocators base_s).
-Proof.
+Proof using EqDecision0 Free Hbase_s IM PreFree PreSubFree SubFree base_s equivocating_IM equivocators index message.
   apply basic_VLSM_weak_embedding.
   - split; [| done].
     by apply lift_sub_to_valid, Hv.
@@ -1088,7 +1089,7 @@ Lemma lift_sub_incl_message_initial
   (m : message)
   (Hm : composite_initial_message_prop sub_IM1 m)
   : composite_initial_message_prop sub_IM2 m.
-Proof.
+Proof using EqDecision0 Hincl IM index indices1 indices2 message sub_IM1 sub_IM2.
   destruct Hm as [[i Hi] Hm].
   unfold sub_IM1, sub_IM in Hm. simpl in Hm.
   apply bool_decide_spec, Hincl in Hi.
@@ -1189,7 +1190,7 @@ Lemma sub_can_emit_sender (P : message -> Prop)
     sender m = Some v ->
     can_emit (pre_loaded_vlsm (free_composite_vlsm sub_IM) P)  m ->
     A v ∈ indices.
-Proof.
+Proof using A EqDecision0 Hsender_safety IM index indices message sender sub_IM validator.
   intros m v Hsender Hemit.
   specialize (Hsender_safety m v Hsender).
   destruct Hemit as [[s om] [[sub_i li] [s' Ht]]].
@@ -1265,7 +1266,7 @@ Qed.
 
 Lemma sub_IM_sender_safety
   : sender_safety_alt_prop sub_IM sub_IM_A sub_IM_sender.
-Proof.
+Proof using A EqDecision0 Hsender_safety IM index indices message sender sub_IM validator.
   intros m sub_v Hsender sub_i Hm.
   destruct_dec_sig sub_v v HAv Heqsub_v.
   destruct_dec_sig sub_i i Hi Heqsub_i.
@@ -1291,7 +1292,7 @@ Lemma sub_IM_has_been_sent_iff_by_sender s
   (Hv : A v ∈ indices)
   : composite_has_been_sent sub_IM s m ->
     has_been_sent (sub_IM (dexist (A v) Hv)) (s (dexist (A v) Hv)) m.
-Proof.
+Proof using A EqDecision0 H Hsender_safety IM index indices message sender sub_IM sub_index_prop_dec validator.
   apply valid_state_has_trace in Hs as Htr.
   destruct Htr as [is [tr Htr]].
   assert (Hsub_sender : sub_IM_sender m = Some (dexist v Hv)).
@@ -1380,7 +1381,7 @@ Lemma sub_IM_no_equivocation_preservation
     l (s, om))
   : composite_no_equivocations_except_from sub_IM
       non_sub_index_authenticated_message l (s, om).
-Proof.
+Proof using A EqDecision0 H Hsender_safety IM can_emit_signed index indices message no_initial_messages_in_IM sender sub_IM validator.
   destruct om as [m |]; [| done].
   destruct Hv as (lX & sX & [_ [=] (_ & Hm & _ & Hc)]).
   specialize (composite_no_initial_valid_messages_have_sender IM A sender
@@ -1589,7 +1590,7 @@ Lemma sub_valid_preloaded_lifts_can_be_emitted
     valid_message_prop (pre_loaded_vlsm (free_composite_vlsm (sub_IM IM (elements indices))) Q) dm)
   : forall m, can_emit (pre_loaded_vlsm (IM j) P) m ->
     can_emit (pre_loaded_vlsm (free_composite_vlsm (sub_IM IM (elements indices))) Q) m.
-Proof.
+Proof using Ci EqDecision0 H5 Hj IM index indices j message.
   intros m Hm.
   eapply VLSM_incl_can_emit.
   - apply (pre_loaded_vlsm_incl_relaxed _ (fun m => Q m \/ P m)).
@@ -1843,7 +1844,7 @@ Context
 *)
 Lemma sub_no_indices_no_can_emit (P : message -> Prop)
   : forall m, ~ can_emit (pre_loaded_vlsm (free_composite_vlsm sub_IM) P) m.
-Proof.
+Proof using EqDecision0 Hno_indices IM index indices message sub_IM.
   apply pre_loaded_empty_composition_no_emit, elem_of_empty_nil.
   by intro sub_i; destruct_dec_sig sub_i i Hi Heqsub_i; subst; inversion Hi.
 Qed.
@@ -1884,7 +1885,7 @@ Context
   `{forall i : index, HasBeenSentCapability (IM i)}
   : forall sub_i : sub_index (elements selection_complement),
     HasBeenSentCapability (sub_IM updated_IM (elements selection_complement) sub_i).
-Proof.
+Proof using Ci EqDecision0 H H0 H1 H2 H3 H4 H5 H6 H7 IM index message replacement_IM selection selection_complement updated_IM.
   intros sub_i.
   unfold sub_IM, updated_IM, update_IM.
   case_decide as Hi; [| typeclasses eauto].
diff --git a/theories/VLSM/Core/TraceableVLSM.v b/theories/VLSM/Core/TraceableVLSM.v
index 6047505f..bbbca9d1 100644
--- a/theories/VLSM/Core/TraceableVLSM.v
+++ b/theories/VLSM/Core/TraceableVLSM.v
@@ -4,6 +4,8 @@ From VLSM.Lib Require Import EquationsExtras.
 From VLSM.Lib Require Import Preamble ListSetExtras.
 From VLSM.Core Require Import VLSM Composition VLSMEmbedding.
 
+Set Default Proof Using "Type".
+
 (** * Traceable VLSMs
 
   This section introduces [TraceableVLSM]s, characterized by the fact that from
@@ -106,7 +108,7 @@ Lemma tv_state_destructor_size :
   forall s' : vstate X, valid_state_prop R s' ->
   forall (s : vstate X) (item : vtransition_item X),
     (item, s) ∈ state_destructor s' -> state_size s < state_size s'.
-Proof.
+Proof using TraceableVLSM0.
   intros.
   apply transition_monotonicity.
   erewrite <- tv_state_destructor_destination by done.
@@ -223,7 +225,7 @@ Qed.
 Lemma composite_tv_state_destructor_destination :
   forall (s' s : composite_state IM) (item : composite_transition_item IM) i,
      (item, s) ∈ composite_state_destructor s' i -> destination item = s'.
-Proof.
+Proof using state_size H0.
   intros *; unfold composite_state_destructor; rewrite elem_of_list_fmap.
   intros ([itemi si] & [= -> ->] & Hin).
   cbn; unfold lift_to_composite_state.
@@ -235,7 +237,7 @@ Lemma composite_tv_state_destructor_transition :
   forall (s : composite_state IM) (item : composite_transition_item IM) (i : index),
   (item, s) ∈ composite_state_destructor s' i ->
   input_valid_transition_item RFree s item.
-Proof.
+Proof using state_size H0.
   intros s' Hs' s item i.
   unfold composite_state_destructor; rewrite elem_of_list_fmap.
   intros ([itemi si] & [=-> ->] & Hin).
@@ -259,7 +261,7 @@ Lemma composite_tv_state_destructor_state_update :
   forall (s : composite_state IM) (item : composite_transition_item IM) (i : index),
   (item, s) ∈ composite_state_destructor s' i ->
   s' = state_update IM s i (destination item i).
-Proof.
+Proof using state_size H0.
   intros s' Hs' s item i Hin.
   replace s' with (destination item) in *
     by (eapply composite_tv_state_destructor_destination; done).
@@ -275,7 +277,7 @@ Lemma composite_tv_state_destructor_initial :
     vinitial_state_prop (IM i) (s i)
       <->
     composite_state_destructor s i = [].
-Proof.
+Proof using state_size H0.
   unfold composite_state_destructor; split; intros Hinit.
   - replace (state_destructor i (s i))
       with (@nil (vtransition_item (IM i) * vstate (IM i))); [done |].
@@ -291,7 +293,7 @@ Lemma composite_tv_state_destructor_reflects_initiality :
   forall (i : index) (s : composite_state IM) (item : composite_transition_item IM),
     (item, s) ∈ composite_state_destructor s' i ->
     forall j, vinitial_state_prop (IM j) (s' j) -> s j = s' j.
-Proof.
+Proof using state_size H0.
   intros s' Hs' i s item Hdestruct.
   apply composite_tv_state_destructor_state_update in Hdestruct as Heqs'; [| done].
   intros j Hinit; destruct (decide (i = j)); subst; [| by state_update_simpl].
@@ -304,7 +306,7 @@ Lemma composite_tv_state_destructor_size :
   forall (s : composite_state IM) (item : composite_transition_item IM) (i : index),
     (item, s) ∈ composite_state_destructor s' i ->
     composite_state_size s < composite_state_size s'.
-Proof.
+Proof using H0.
   intros s' Hs' s item i.
   unfold composite_state_destructor; rewrite elem_of_list_fmap.
   intros ([itemi si] & [= -> ->] & Hin).
@@ -320,7 +322,7 @@ Lemma composite_state_destructor_lookup_reachable :
   forall s' : composite_state IM, valid_state_prop RFree s' ->
   forall i n item s, composite_state_destructor s' i !! n = Some (item, s) ->
     input_valid_transition_item RFree s item.
-Proof.
+Proof using state_size H0.
   intros s' Hs' i n item s Hdestruct.
   by eapply composite_tv_state_destructor_transition, elem_of_list_lookup_2.
 Qed.
@@ -329,7 +331,7 @@ Lemma composite_state_destructor_head_reachable :
   forall s' : composite_state IM, valid_state_prop RFree s' ->
   forall i item s, head (composite_state_destructor s' i) = Some (item, s) ->
   input_valid_transition_item RFree s item.
-Proof.
+Proof using state_size H0.
   intros s' Hs' i item s Hdestruct.
   by eapply composite_tv_state_destructor_transition, head_Some_elem_of.
 Qed.
@@ -386,7 +388,7 @@ Lemma choosing_well_position_exists :
     (i_n :=  choose s' Hs' indices),
       composite_state_destructor s' i_n.1 <> [] ->
       composite_state_destructor s' i_n.1 !! i_n.2 <> None.
-Proof.
+Proof using state_size H0.
   intros choose s' Hs' indices Hchoose i_n Hdestruct.
   eapply not_eq_None_Some, cw_chosen_position_exists; [done | |].
   - by destruct (choose _ _ _).
@@ -417,7 +419,7 @@ Lemma composite_tv_state_destructor_preserves_not_in_indices_initial  :
     forall (indices : list index),
       not_in_indices_initial_prop s' indices ->
       not_in_indices_initial_prop s indices.
-Proof.
+Proof using state_size H0.
   intros s' Hs' * Heq indices Hinits' j Hj.
   by erewrite composite_tv_state_destructor_reflects_initiality;
     [apply Hinits' | | eapply elem_of_list_lookup_2 | apply Hinits'].
@@ -434,7 +436,7 @@ Lemma set_remove_preserves_not_in_indices_initial :
   forall (indices : list index),
   not_in_indices_initial_prop s' indices ->
   not_in_indices_initial_prop s' (StdppListSet.set_remove i indices).
-Proof.
+Proof using state_size H0.
   intros s' Hs' i Hdestruct indices Hinit j Hj.
   destruct (decide (j ∈ indices)); [| by apply Hinit].
   destruct (decide (j = i)); [by subst; apply composite_tv_state_destructor_initial |].
diff --git a/theories/VLSM/Core/VLSM.v b/theories/VLSM/Core/VLSM.v
index 896ebb9f..0b361dca 100644
--- a/theories/VLSM/Core/VLSM.v
+++ b/theories/VLSM/Core/VLSM.v
@@ -3,6 +3,8 @@ From stdpp Require Import prelude.
 From Coq Require Import Streams.
 From VLSM.Lib Require Import Preamble ListExtras StreamExtras.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Basics
 
   This module provides basic VLSM infrastructure.
@@ -2767,7 +2769,7 @@ Proof. by subst. Qed.
 
 Lemma same_VLSM_initial_message_preservation m
   : vinitial_message_prop X1 m -> vinitial_message_prop X2 m.
-Proof. by subst. Qed.
+Proof using Heq. by subst. Qed.
 
 End sec_same_VLSM.
 
@@ -2848,7 +2850,7 @@ Lemma history_unique_trace_to_reachable :
   forall is s tr, finite_valid_trace_init_to R is s tr ->
   forall is' tr', finite_valid_trace_init_to R is' s tr' ->
     is' = is /\ tr' = tr.
-Proof.
+Proof using H.
   intros is s tr Htr; induction Htr using finite_valid_trace_init_to_rev_ind;
     intros is' tr' [Htr' His'].
   - destruct_list_last tr' tr'' item Heqtr'; [by inversion Htr' | subst].
diff --git a/theories/VLSM/Core/VLSMProjections.v b/theories/VLSM/Core/VLSMProjections.v
index ab0e04c7..f5f5233a 100644
--- a/theories/VLSM/Core/VLSMProjections.v
+++ b/theories/VLSM/Core/VLSMProjections.v
@@ -6,6 +6,8 @@ From VLSM.Core Require Export VLSMPartialProjection VLSMStutteringEmbedding.
 From VLSM.Core Require Export VLSMTotalProjection VLSMEmbedding.
 From VLSM.Core Require Export VLSMInclusion VLSMEquality.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Projection Properties *)
 
 Section sec_same_VLSM_embedding.
diff --git a/theories/VLSM/Core/Validator.v b/theories/VLSM/Core/Validator.v
index b11c97e8..36ab83d1 100644
--- a/theories/VLSM/Core/Validator.v
+++ b/theories/VLSM/Core/Validator.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From VLSM.Core Require Import VLSM VLSMProjections Composition.
 
+Set Default Proof Using "Type".
+
 (** * VLSM Projection Validators
 
   In the sequel we fix VLSMs <<X>> and <<Y>> and some <<label_project>>
@@ -300,7 +302,7 @@ Context
 Lemma projection_induced_valid_message_char
   : forall om, option_valid_message_prop projection_induced_validator om ->
     option_valid_message_prop X om.
-Proof.
+Proof using Htransition_consistency Htransition_Some Hstate_lift Hlabel_lift.
   intros om [s Hsom].
   induction Hsom.
   - by destruct om as [m |]; [done |]; apply option_valid_message_None.
@@ -322,7 +324,7 @@ Context
 
 Lemma projection_induced_validator_is_projection
   : VLSM_projection X pre_projection_induced_validator label_project state_project.
-Proof.
+Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hlabel_lift.
   apply basic_VLSM_projection; intro; intros.
   - by exists lX, s.
   - specialize (Htransition_Some _ _ H _ _ _ _ H0); cbn.
@@ -344,7 +346,7 @@ Lemma induced_validator_transition_item_lift
   : pre_VLSM_projection_transition_item_project _ _ label_project state_project
     (pre_VLSM_embedding_transition_item_project _ _ label_lift state_lift item)
     = Some item.
-Proof.
+Proof using Hstate_lift Hlabel_lift.
   destruct item.
   unfold pre_VLSM_embedding_transition_item_project,
          pre_VLSM_projection_transition_item_project.
@@ -356,7 +358,7 @@ Lemma induced_validator_trace_lift
   : pre_VLSM_projection_finite_trace_project _ _ label_project state_project
     (pre_VLSM_embedding_finite_trace_project _ _ label_lift state_lift tr)
     = tr.
-Proof.
+Proof using Hstate_lift Hlabel_lift.
   induction tr; cbn; [done |].
   by rewrite induced_validator_transition_item_lift; f_equal.
 Qed.
@@ -423,7 +425,7 @@ Lemma projection_induced_validator_incl
   (Htransition_consistency2 :
     induced_validator_transition_consistency_Some X2 TY label_project state_project)
   : VLSM_incl X1 X2 -> VLSM_incl XY1 XY2.
-Proof.
+Proof using Hstate_lift Hlabel_lift.
   pose (Htransition_Some1 :=
     basic_weak_projection_transition_consistency_Some
       X1 TY _ _ _ _ Hlabel_lift Hstate_lift Htransition_consistency1).
@@ -479,7 +481,7 @@ Lemma projection_induced_validator_eq
   (Htransition_consistency2 :
     induced_validator_transition_consistency_Some X2 TY label_project state_project)
   : VLSM_eq X1 X2 -> VLSM_eq XY1 XY2.
-Proof.
+Proof using Hstate_lift Hlabel_lift.
   intro Heq; apply VLSM_eq_incl_iff; split.
   - by apply (projection_induced_validator_incl MX1 MX2); [.. | apply VLSM_eq_proj1].
   - by apply (projection_induced_validator_incl MX2 MX1); [.. | apply VLSM_eq_proj2].
@@ -530,7 +532,7 @@ Context
 Lemma projection_induced_valid_transition_eq
   : forall l s om, vvalid Xi l (s, om) ->
     vtransition Xi l (s, om) = vtransition Y l (s, om).
-Proof.
+Proof using Htransition_consistency Htransition_None Hstate_lift Hproji Hproj Hlabel_lift.
   intros l s im (lX & sX & [Hlx HsX Hv]); cbn in HsX; subst s.
   replace (vtransition Y _ _) with
     (state_project (vtransition X lX (sX, im)).1, (vtransition X lX (sX, im)).2).
@@ -543,7 +545,7 @@ Qed.
 
 Lemma induced_validator_incl_preloaded_with_all_messages
   : VLSM_incl Xi PreY.
-Proof.
+Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift.
   apply basic_VLSM_incl.
   - by intros is (s & <- & Hs); apply (VLSM_projection_initial_state Hproj).
   - by intros l s m Hv HsY HmX; apply initial_message_is_valid.
@@ -574,7 +576,7 @@ Definition projection_validator_prop_alt :=
 Lemma validator_alt_free_states_are_projection_states
   : projection_validator_prop_alt ->
     forall s, valid_state_prop PreY s -> valid_state_prop Xi s.
-Proof.
+Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift.
   intros Hvalidator sY Hs.
   induction Hs using valid_state_prop_ind.
   - apply initial_state_is_valid.
@@ -598,7 +600,7 @@ Qed.
 (** Below we show that the two definitions above are actually equivalent. *)
 Lemma projection_validator_prop_alt_iff
   : projection_validator_prop_alt <-> projection_validator_prop Y label_project state_project.
-Proof.
+Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift.
   split; intros Hvalidator l si om Hvalid.
   - apply Hvalidator; [by apply Hvalid |].
     by apply validator_alt_free_states_are_projection_states; [.. | apply Hvalid].
@@ -612,7 +614,7 @@ Qed.
 Lemma validator_free_states_are_projection_states
   : projection_validator_prop Y label_project state_project ->
     forall s, valid_state_prop PreY s -> valid_state_prop Xi s.
-Proof.
+Proof using Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift.
   rewrite <- projection_validator_prop_alt_iff by done.
   by apply validator_alt_free_states_are_projection_states.
 Qed.
@@ -631,7 +633,7 @@ Context
 *)
 Lemma pre_loaded_with_all_messages_validator_proj_incl
   : VLSM_incl PreY Xi.
-Proof.
+Proof using Hvalidator Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift.
   (* reduce inclusion to inclusion of finite traces. *)
   apply VLSM_incl_finite_traces_characterization.
   intros sY trY HtrY.
@@ -661,7 +663,7 @@ Qed.
 *)
 Lemma pre_loaded_with_all_messages_validator_proj_eq
   : VLSM_eq PreY Xi.
-Proof.
+Proof using Hvalidator Htransition_consistency Htransition_Some Htransition_None Hstate_lift Hproji Hproj Hlabel_lift Hinitial_lift.
   apply VLSM_eq_incl_iff; split.
   - by apply pre_loaded_with_all_messages_validator_proj_incl.
   - by apply induced_validator_incl_preloaded_with_all_messages.
@@ -973,7 +975,7 @@ Context
 
 Lemma pre_loaded_with_all_messages_self_validator_vlsm_incl
   : VLSM_incl PreX X.
-Proof.
+Proof using Hvalidator.
   unfold self_validator_vlsm_prop  in Hvalidator.
   destruct X as (T & M). simpl in *.
   (* redcuction to inclusion of finite traces. *)
@@ -997,7 +999,7 @@ Qed.
 
 Lemma pre_loaded_with_all_messages_self_validator_vlsm_eq
   : VLSM_eq PreX X.
-Proof.
+Proof using Hvalidator.
   split.
   - by apply pre_loaded_with_all_messages_self_validator_vlsm_incl.
   - pose (vlsm_incl_pre_loaded_with_all_messages_vlsm X) as Hincl.
diff --git a/theories/VLSM/Lib/Ctauto.v b/theories/VLSM/Lib/Ctauto.v
index 1ec32072..52b74f7b 100644
--- a/theories/VLSM/Lib/Ctauto.v
+++ b/theories/VLSM/Lib/Ctauto.v
@@ -1,5 +1,7 @@
 From Cdcl Require Export Itauto.
 
+Set Default Proof Using "Type".
+
 (** * Classical Itauto tactic *)
 
 Ltac gen_conflicts tac :=
diff --git a/theories/VLSM/Lib/EquationsExtras.v b/theories/VLSM/Lib/EquationsExtras.v
index 03d008cc..60fe92a4 100644
--- a/theories/VLSM/Lib/EquationsExtras.v
+++ b/theories/VLSM/Lib/EquationsExtras.v
@@ -1,5 +1,7 @@
 From Equations Require Export Equations.
 
+Set Default Proof Using "Type".
+
 (** * Equations utility definitions
 
   The definition of [inspect] is available in Equations as of version 1.3+8.16.
diff --git a/theories/VLSM/Lib/FinExtras.v b/theories/VLSM/Lib/FinExtras.v
index 3127e53a..5671beb2 100644
--- a/theories/VLSM/Lib/FinExtras.v
+++ b/theories/VLSM/Lib/FinExtras.v
@@ -1,5 +1,7 @@
 From stdpp Require Import prelude.
 
+Set Default Proof Using "Type".
+
 (** * Finite type utility definitions and lemmas *)
 
 Fixpoint up_to_n_listing
diff --git a/theories/VLSM/Lib/FinFunExtras.v b/theories/VLSM/Lib/FinFunExtras.v
index dee9d20c..3d51c30f 100644
--- a/theories/VLSM/Lib/FinFunExtras.v
+++ b/theories/VLSM/Lib/FinFunExtras.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude finite.
 From Coq Require Import FinFun.
 From VLSM.Lib Require Import Preamble ListExtras StdppExtras.
 
+Set Default Proof Using "Type".
+
 (** * Finite function utility definitions and lemmas *)
 
 Lemma listing_from_finite (A : Type) `{finite.Finite A} : Listing (enum A).
diff --git a/theories/VLSM/Lib/FinSetExtras.v b/theories/VLSM/Lib/FinSetExtras.v
index 67c0fdf7..5a757d7e 100644
--- a/theories/VLSM/Lib/FinSetExtras.v
+++ b/theories/VLSM/Lib/FinSetExtras.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble.
 
+Set Default Proof Using "Type".
+
 (** * Finite set utility definitions and lemmas *)
 
 Section sec_fin_set.
@@ -13,12 +15,12 @@ Section sec_general.
 
 Lemma elements_subseteq (X Y : C) :
   X ⊆ Y -> elements X ⊆ elements Y.
-Proof. by set_solver. Qed.
+Proof using H6 H4 H3 H2 H1 H0 EqDecision0. by set_solver. Qed.
 
 Lemma union_size_ge_size1
   (X Y : C) :
   size (X ∪ Y) >= size X.
-Proof.
+Proof using H6 H4 H3 H1 H0 H EqDecision0.
   apply subseteq_size.
   apply subseteq_union.
   by set_solver.
@@ -27,7 +29,7 @@ Qed.
 Lemma union_size_ge_size2
   (X Y : C) :
   size (X ∪ Y) >= size Y.
-Proof.
+Proof using H6 H4 H3 H1 H0 H EqDecision0.
   apply subseteq_size.
   apply subseteq_union.
   by set_solver.
@@ -36,7 +38,7 @@ Qed.
 Lemma union_size_ge_average
   (X Y : C) :
   2 * size (X ∪ Y) >= size X + size Y.
-Proof.
+Proof using H6 H4 H3 H1 H0 H EqDecision0.
   specialize (union_size_ge_size1 X Y) as Hx.
   specialize (union_size_ge_size2 X Y) as Hy.
   by lia.
@@ -45,7 +47,7 @@ Qed.
 Lemma difference_size_le_self
   (X Y : C) :
   size (X ∖  Y) <= size X.
-Proof.
+Proof using H6 H3 H2 H1 H0 H EqDecision0.
   apply subseteq_size.
   apply elem_of_subseteq.
   intros x Hx.
@@ -56,7 +58,7 @@ Qed.
 Lemma union_size_le_sum
   (X Y : C) :
   size (X ∪ Y) <= size X + size Y.
-Proof.
+Proof using H6 H4 H3 H1 H0 H EqDecision0.
   specialize (size_union_alt X Y) as Halt.
   rewrite Halt.
   specialize (difference_size_le_self Y X).
@@ -66,7 +68,7 @@ Qed.
 Lemma intersection_size1
   (X Y : C) :
   size (X ∩ Y) <= size X.
-Proof.
+Proof using H6 H4 H2 H1 H0 H EqDecision0.
   apply (subseteq_size (X ∩ Y) X).
   by set_solver.
 Qed.
@@ -74,7 +76,7 @@ Qed.
 Lemma intersection_size2
   (X Y : C) :
   size (X ∩ Y) <= size Y.
-Proof.
+Proof using H6 H4 H2 H1 H0 H EqDecision0.
   apply (subseteq_size (X ∩ Y) Y).
   by set_solver.
 Qed.
@@ -83,7 +85,7 @@ Lemma difference_size_subset
   (X Y : C)
   (Hsub : Y ⊆ X) :
   (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size Y))%Z.
-Proof.
+Proof using H6 H3 H2 H1 H0 EqDecision0.
   assert (Htemp : Y ∪ (X ∖ Y) ≡ X).
   {
     apply set_equiv_equivalence.
@@ -114,14 +116,14 @@ Qed.
 Lemma difference_with_intersection
   (X Y : C) :
   X ∖ Y ≡ X ∖ (X ∩ Y).
-Proof.
+Proof using H6 H5 H2 H1 H0 EqDecision0.
   by set_solver.
 Qed.
 
 Lemma difference_size
   (X Y : C) :
   (Z.of_nat (size (X ∖ Y)) = Z.of_nat (size X) - Z.of_nat (size (X ∩ Y)))%Z.
-Proof.
+Proof using H6 H2 H1 H0 H EqDecision0.
   rewrite difference_with_intersection.
   specialize (difference_size_subset X (X ∩ Y)) as Hdif.
   by set_solver.
@@ -130,7 +132,7 @@ Qed.
 Lemma difference_size_ge_disjoint_case
   (X Y : C) :
   size (X ∖ Y) >= size X - size Y.
-Proof.
+Proof using H6 H3 H2 H1 H0 H EqDecision0.
   specialize (difference_size X Y).
   specialize (intersection_size2 X Y).
   by lia.
@@ -139,7 +141,7 @@ Qed.
 Lemma list_to_set_size
   (l : list A) :
   size (list_to_set l (C := C)) <= length l.
-Proof.
+Proof using H6 H4 H3 H EqDecision0.
   induction l; cbn.
   - by rewrite size_empty; lia.
   - specialize (union_size_le_sum ({[ a ]}) (list_to_set l)) as Hun_size.
@@ -159,7 +161,7 @@ Context
 Lemma filter_subset
   (Hsub : X ⊆ Y) :
   filter P X ⊆ filter P Y.
-Proof.
+Proof using H6 H4 H3 EqDecision0.
   intros a HaX.
   apply elem_of_filter in HaX.
   apply elem_of_filter.
@@ -169,7 +171,7 @@ Qed.
 Lemma filter_subprop
   (Hsub : forall a, (P a -> P2 a)) :
   filter P X ⊆ filter P2 X.
-Proof.
+Proof using H6 H4 H3 EqDecision0.
   intros a HaP.
   apply elem_of_filter in HaP.
   apply elem_of_filter.
@@ -191,7 +193,7 @@ Lemma set_map_subset
   (X Y : C)
   (Hsub : X ⊆ Y) :
   set_map (D := D) f X ⊆ set_map (D := D) f Y.
-Proof.
+Proof using H6 H4 H3 H2 H14 H13 H12 H11 H1 H0 EqDecision1 EqDecision0.
   intros a Ha.
   apply elem_of_map in Ha.
   apply elem_of_map.
@@ -202,7 +204,7 @@ Lemma set_map_size_upper_bound
   (f : A -> B)
   (X : C) :
   size (set_map (D := D) f X) <= size X.
-Proof.
+Proof using H7 H14 H12 H11 EqDecision1.
   unfold set_map.
   remember (f <$> elements X) as fX.
   set (x := size (list_to_set _)).
@@ -215,7 +217,7 @@ Qed.
 
 Lemma elem_of_set_map_inj (f : A -> B) `{!Inj (=) (=) f} (a : A) (X : C) :
   f a ∈@{D} fin_sets.set_map f X <-> a ∈ X.
-Proof.
+Proof using H6 H4 H3 H2 H14 H13 H12 H11 H1 H0 EqDecision1 EqDecision0.
   intros; rewrite elem_of_map.
   split; [| by eexists].
   intros (_v & HeqAv & H_v).
@@ -224,6 +226,6 @@ Proof.
 Qed.
 
 Lemma set_map_id (X : C) : X ≡ set_map id X.
-Proof. by set_solver. Qed.
+Proof using H9 H8 H7 H6 H4 H3 H14 H13 H12 H11 H10 EqDecision1 EqDecision0 D B. by set_solver. Qed.
 
 End sec_map.
diff --git a/theories/VLSM/Lib/Itauto.v b/theories/VLSM/Lib/Itauto.v
index 468d0408..ac21ec77 100644
--- a/theories/VLSM/Lib/Itauto.v
+++ b/theories/VLSM/Lib/Itauto.v
@@ -1,5 +1,7 @@
 From Cdcl Require Export Itauto.
 
+Set Default Proof Using "Type".
+
 (** * Constructive Itauto tactic *)
 
 Ltac gen_conflicts tac :=
diff --git a/theories/VLSM/Lib/ListExtras.v b/theories/VLSM/Lib/ListExtras.v
index d795e9b4..98c05fd2 100644
--- a/theories/VLSM/Lib/ListExtras.v
+++ b/theories/VLSM/Lib/ListExtras.v
@@ -3,6 +3,8 @@ From stdpp Require Import finite.
 From Coq Require Import FinFun.
 From VLSM.Lib Require Import Preamble.
 
+Set Default Proof Using "Type".
+
 (** * Utility lemmas about lists *)
 
 (** A list is empty if it has no members. *)
diff --git a/theories/VLSM/Lib/ListFinSetExtras.v b/theories/VLSM/Lib/ListFinSetExtras.v
index 57f3f021..6695ac41 100644
--- a/theories/VLSM/Lib/ListFinSetExtras.v
+++ b/theories/VLSM/Lib/ListFinSetExtras.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble StdppListFinSet.
 
+Set Default Proof Using "Type".
+
 Section sec_defs.
 
 Context `{FinSet A C}.
@@ -20,11 +22,11 @@ Definition set_diff (x y : set) : set := x ∖ y.
 
 Lemma set_union_subseteq_left :
   forall (s1 s2 : set), s1 ⊆ set_union s1 s2.
-Proof. by intros s1 s2 x Hincl; apply set_union_intro; left. Qed.
+Proof using H6 H5 H4 H3 H1 H0 EqDecision0. by intros s1 s2 x Hincl; apply set_union_intro; left. Qed.
 
 Lemma set_union_subseteq_iff :
   forall (s1 s2 s : set), set_union s1 s2 ⊆ s <-> s1 ⊆ s /\ s2 ⊆ s.
-Proof.
+Proof using H6 H5 H4 H3 H1 H0 EqDecision0.
   intros s1 s2 s.
   unfold subseteq, set_subseteq_instance, set_subseteq_instance.
   setoid_rewrite set_union_iff.
@@ -37,7 +39,7 @@ Proof. by intros a s1 s2 Ha Hincl; apply Hincl. Qed.
 
 Lemma empty_subseteq :
   forall (s : set), ∅ ⊆ s.
-Proof. by intros s x Hin; contradict Hin; apply not_elem_of_empty. Qed.
+Proof using H6 H5 H4 H3 H2 H1 EqDecision0. by intros s x Hin; contradict Hin; apply not_elem_of_empty. Qed.
 
 #[export] Instance elem_of_dec : RelDecision (@elem_of A C _) := elem_of_dec_slow.
 
diff --git a/theories/VLSM/Lib/ListSetExtras.v b/theories/VLSM/Lib/ListSetExtras.v
index 390c4413..d9d97a87 100644
--- a/theories/VLSM/Lib/ListSetExtras.v
+++ b/theories/VLSM/Lib/ListSetExtras.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble ListExtras StdppExtras StdppListSet.
 
+Set Default Proof Using "Type".
+
 (** * List set utility definitions and lemmas *)
 
 Definition set_eq {A} (s1 s2 : set A) : Prop :=
diff --git a/theories/VLSM/Lib/Measurable.v b/theories/VLSM/Lib/Measurable.v
index 41f3a53f..14b5c25d 100644
--- a/theories/VLSM/Lib/Measurable.v
+++ b/theories/VLSM/Lib/Measurable.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From Coq Require Import Reals Lra.
 From VLSM.Lib Require Import Preamble ListExtras StdppListSet StdppListFinSet.
 
+Set Default Proof Using "Type".
+
 (** * Measure-related definitions and lemmas *)
 
 Definition pos_R := {r : R | (r > 0)%R}.
@@ -29,7 +31,7 @@ Proof. done. Qed.
 
 Lemma sum_weights_empty :
   forall (l : Cv), l ≡ ∅ -> sum_weights l = 0%R.
-Proof.
+Proof using H7 H5 H4 H3 H2 EqDecision0.
   intros l Hl.
   unfold sum_weights, set_fold; cbn.
   by apply elements_empty_iff in Hl as ->.
@@ -80,7 +82,7 @@ Lemma sum_weights_subseteq_list
   NoDup vs' ->
   vs ⊆ vs' ->
   (sum_weights_list vs <= sum_weights_list vs')%R.
-Proof.
+Proof using EqDecision0.
   induction vs; intros vs' Hnodup_vs Hnodup_vs' Hincl;
     [by apply sum_weights_positive_list |].
   pose proof (Hvs' := sum_weights_in_list a vs' Hnodup_vs').
@@ -100,7 +102,7 @@ Lemma sum_weights_subseteq
   : forall (vs vs' : Cv),
   vs ⊆ vs' ->
   (sum_weights vs <= sum_weights vs')%R.
-Proof.
+Proof using H7 H5 H4 H3 H2 H1 EqDecision0.
   intros vs vs' Hincl.
   rewrite !sum_weights_list_rew.
   apply sum_weights_subseteq_list.
@@ -110,7 +112,7 @@ Proof.
 Qed.
 
 Lemma sum_weights_proper : Proper (equiv ==> eq) sum_weights.
-Proof.
+Proof using H7 H5 H4 H3 H2 H1 EqDecision0.
   intros x y Hequiv.
   by apply Rle_antisym; apply sum_weights_subseteq; intro a; apply Hequiv.
 Qed.
@@ -118,7 +120,7 @@ Qed.
 Lemma sum_weights_in :
   forall v (vs : Cv),
     v ∈ vs -> sum_weights vs = (proj1_sig (weight v) + sum_weights (set_remove v vs))%R.
-Proof.
+Proof using H7 H4 H3 H1 EqDecision0.
   intros v vs Hv.
   rewrite sum_weights_list_rew, sum_weights_in_list with (v := v); cycle 1.
   - by apply NoDup_elements.
@@ -159,7 +161,7 @@ Lemma sum_weights_disj_union :
   forall (vs vs' : Cv),
     vs ## vs' ->
     sum_weights (vs ∪ vs') = (sum_weights vs + sum_weights vs')%R.
-Proof.
+Proof using H7 H5 H4 H2 H1 EqDecision0.
   intros vs vs' Hdisj.
   apply elements_disj_union, sum_weights_list_permutation_proper in Hdisj.
   setoid_rewrite Hdisj.
@@ -168,7 +170,7 @@ Qed.
 
 Lemma sum_weights_union_empty (vs : Cv) :
   sum_weights (vs ∪ ∅) = sum_weights vs.
-Proof.
+Proof using H7 H5 H4 H2 H0 EqDecision0.
   rewrite sum_weights_disj_union by apply disjoint_empty_r.
   by rewrite (sum_weights_empty ∅); [lra |].
 Qed.
diff --git a/theories/VLSM/Lib/NatExtras.v b/theories/VLSM/Lib/NatExtras.v
index c1d5ef43..2a308511 100644
--- a/theories/VLSM/Lib/NatExtras.v
+++ b/theories/VLSM/Lib/NatExtras.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From VLSM.Lib Require Import EquationsExtras.
 From VLSM.Lib Require Import Preamble.
 
+Set Default Proof Using "Type".
+
 (** * Natural number utility definitions and lemmas
 
   Given a decidable property on naturals and a bound, finds the
diff --git a/theories/VLSM/Lib/NeList.v b/theories/VLSM/Lib/NeList.v
index 397611f6..eca8cd16 100644
--- a/theories/VLSM/Lib/NeList.v
+++ b/theories/VLSM/Lib/NeList.v
@@ -1,6 +1,8 @@
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import ListExtras StdppExtras.
 
+Set Default Proof Using "Type".
+
 (** A straight-forward inductive definition of non-empty lists. *)
 Inductive ne_list (A : Type) : Type :=
 | nel_singl : A -> ne_list A
diff --git a/theories/VLSM/Lib/Preamble.v b/theories/VLSM/Lib/Preamble.v
index dfd89b02..f78610a4 100644
--- a/theories/VLSM/Lib/Preamble.v
+++ b/theories/VLSM/Lib/Preamble.v
@@ -3,6 +3,8 @@ Obligation Tactic := idtac.
 From stdpp Require Import prelude.
 From Coq Require Import Eqdep_dec.
 
+Set Default Proof Using "Type".
+
 (** * General utility definitions, lemmas, and tactics *)
 
 Tactic Notation "spec" hyp(H) :=
@@ -217,7 +219,7 @@ Proof. by induction n; cbn; [| case_decide]; lia. Qed.
 
 #[local] Lemma find_least_among_helper_has_property :
   forall n, P (find_least_among_helper n).
-Proof. by induction n; cbn; [| case_decide]. Qed.
+Proof using Hbound. by induction n; cbn; [| case_decide]. Qed.
 
 #[local] Lemma find_least_among_helper_minimal :
   forall n m,
@@ -235,7 +237,7 @@ Qed.
     minimal_among le
       (fun m => bound - n <= m <= bound /\ P m)
       (find_least_among_helper n).
-Proof.
+Proof using Hbound.
   split; [split |].
   - by apply find_least_among_helper_bounded.
   - by apply find_least_among_helper_has_property.
@@ -246,7 +248,7 @@ Qed.
 
 Lemma find_least_among_is_minimal
   : minimal_among le P find_least_among.
-Proof.
+Proof using Hbound.
   destruct (find_least_among_helper_is_minimal bound) as [[[_ ?] ?] Hmin'].
   split; [done |].
   intros; apply Hmin'; [| done].
diff --git a/theories/VLSM/Lib/RealsExtras.v b/theories/VLSM/Lib/RealsExtras.v
index 372e9992..b364badf 100644
--- a/theories/VLSM/Lib/RealsExtras.v
+++ b/theories/VLSM/Lib/RealsExtras.v
@@ -1,6 +1,8 @@
 From Coq Require Import Reals.
 From stdpp Require Import prelude.
 
+Set Default Proof Using "Type".
+
 (** * Real number utility definitions and lemmas *)
 
 (** Sum a list of real numbers. *)
diff --git a/theories/VLSM/Lib/SortedLists.v b/theories/VLSM/Lib/SortedLists.v
index ab4a3791..e50e6f18 100644
--- a/theories/VLSM/Lib/SortedLists.v
+++ b/theories/VLSM/Lib/SortedLists.v
@@ -3,6 +3,8 @@ From stdpp Require Import prelude.
 From Coq Require Import Sorting.
 From VLSM.Lib Require Import Preamble ListExtras ListSetExtras.
 
+Set Default Proof Using "Type".
+
 (** * Sorted list utility functions and lemmas *)
 
 Fixpoint list_compare {A} (compare : A -> A -> comparison)
diff --git a/theories/VLSM/Lib/StdppExtras.v b/theories/VLSM/Lib/StdppExtras.v
index a305f3c4..08e03963 100644
--- a/theories/VLSM/Lib/StdppExtras.v
+++ b/theories/VLSM/Lib/StdppExtras.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble ListExtras.
 
+Set Default Proof Using "Type".
+
 (** * Std++ Related Results *)
 
 Lemma elem_of_take {A : Type} (l : list A) (n : nat) (x : A) :
diff --git a/theories/VLSM/Lib/StdppListFinSet.v b/theories/VLSM/Lib/StdppListFinSet.v
index 8772468b..2a7851be 100644
--- a/theories/VLSM/Lib/StdppListFinSet.v
+++ b/theories/VLSM/Lib/StdppListFinSet.v
@@ -1,6 +1,8 @@
 From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 
+Set Default Proof Using "Type".
+
 (** * Finite set implementation of a list set interface *)
 
 Section sec_fst_defs.
@@ -21,14 +23,14 @@ Definition set_diff (x y : set) : set := x ∖ y.
 
 Lemma set_add_intro1 :
   forall (a b : A) (x : set), a ∈ x -> a ∈ set_add b x.
-Proof.
+Proof using H6 H5 H4 H3 H0 EqDecision0.
   unfold set_add; intros a b x Hab.
   by apply elem_of_union; right.
 Qed.
 
 Lemma set_add_intro2 :
   forall (a b : A) (x : set), a = b -> a ∈ set_add b x.
-Proof.
+Proof using H6 H5 H4 H3 H0 EqDecision0.
   unfold set_add; intros a b x Hab.
   by rewrite elem_of_union, elem_of_singleton; left.
 Qed.
@@ -37,21 +39,21 @@ Qed.
 
 Lemma set_add_intro :
   forall (a b : A) (x : set), a = b \/ a ∈ x -> a ∈ set_add b x.
-Proof.
+Proof using H6 H5 H4 H3 H0 EqDecision0.
   unfold set_add; intros a b x Hab.
   by rewrite elem_of_union, elem_of_singleton.
 Qed.
 
 Lemma set_add_elim :
   forall (a b : A) (x : set), a ∈ set_add b x -> a = b \/ a ∈ x.
-Proof.
+Proof using H6 H5 H4 H3 H0 EqDecision0.
   unfold set_add; intros a b x Hab.
   by rewrite elem_of_union, elem_of_singleton in Hab.
 Qed.
 
 Lemma set_add_not_empty :
   forall (a : A) (x : set), ¬ set_add a x ≡ ∅.
-Proof.
+Proof using H6 H5 H4 H3 EqDecision0.
   unfold set_add; intros a x Hcontra.
   cut (a ∈@{C} ∅); [by apply not_elem_of_empty |].
   by rewrite <- Hcontra, elem_of_union, elem_of_singleton; left.
@@ -59,7 +61,7 @@ Qed.
 
 Lemma set_add_iff a b l :
   a ∈ set_add b l <-> a = b \/ a ∈ l.
-Proof.
+Proof using H6 H5 H4 H3 H0 EqDecision0.
   split.
   - by apply set_add_elim.
   - by apply set_add_intro.
@@ -67,14 +69,14 @@ Qed.
 
 Lemma set_remove_1 (a b : A) (l : set) :
   a ∈ set_remove b l -> a ∈ l.
-Proof.
+Proof using H6 H5 H3 H2 H0 EqDecision0.
   unfold set_remove; intros Habl.
   by apply elem_of_difference in Habl as [Hl Hnb]. 
 Qed.
 
 Lemma set_remove_2 (a b : A) (l : set) :
   a ∈ set_remove b l -> a <> b.
-Proof.
+Proof using H6 H5 H3 H2 H0 EqDecision0.
   unfold set_remove; intros Habl.
   rewrite elem_of_difference, elem_of_singleton in Habl.
   by destruct Habl.
@@ -82,14 +84,14 @@ Qed.
 
 Lemma set_remove_3 (a b : A) (l : set) :
   a ∈ l -> a <> b -> a ∈ set_remove b l.
-Proof.
+Proof using H6 H5 H3 H2 H0 EqDecision0.
   intros Hl Hnb; unfold set_remove.
   by rewrite elem_of_difference, elem_of_singleton.
 Qed.
 
 Lemma set_remove_iff (a b : A) (l : set) :
   a ∈ set_remove b l <-> a ∈ l /\ a <> b.
-Proof.
+Proof using H6 H5 H3 H2 H0 EqDecision0.
   split; [split |].
   - by eapply set_remove_1.
   - by eapply set_remove_2.
@@ -99,20 +101,20 @@ Qed.
 Lemma set_union_intro :
   forall (a : A) (x y : set),
     a ∈ x \/ a ∈ y -> a ∈ set_union x y.
-Proof.
+Proof using H6 H5 H4 H3 H1 H0 EqDecision0.
   by intros; apply elem_of_union.
 Qed.
 
 Lemma set_union_elim :
   forall (a : A) (x y : set),
     a ∈ set_union x y -> a ∈ x \/ a ∈ y.
-Proof.
+Proof using H6 H5 H4 H3 H1 H0 EqDecision0.
   by intros; apply elem_of_union.
 Qed.
 
 Lemma set_union_iff a l l' :
   a ∈ set_union l l' <-> a ∈ l \/ a ∈ l'.
-Proof.
+Proof using H6 H5 H4 H3 H1 H0 EqDecision0.
   split.
   - by apply set_union_elim.
   - by apply set_union_intro.
@@ -121,28 +123,28 @@ Qed.
 Lemma set_diff_intro :
   forall (a : A) (x y : set),
     a ∈ x -> a ∉ y -> a ∈ set_diff x y.
-Proof.
+Proof using H6 H5 H3 H2 H1 H0 EqDecision0.
   by intros; apply elem_of_difference.
 Qed.
 
 Lemma set_diff_elim1 :
   forall (a : A) (x y : set),
     a ∈ set_diff x y -> a ∈ x.
-Proof.
+Proof using H6 H5 H3 H2 H1 H0 EqDecision0.
   unfold set_diff; intros a x y Hxy.
   by apply elem_of_difference in Hxy as [Hx _].
 Qed.
 
 Lemma set_diff_elim2 :
   forall (a : A) (x y : set), a ∈ set_diff x y -> a ∉ y.
-Proof.
+Proof using H6 H5 H3 H2 H1 H0 EqDecision0.
   unfold set_diff; intros a x y Hxy.
   by apply elem_of_difference in Hxy as [_ Hny].
 Qed.
 
 Lemma set_diff_iff a l l' :
   a ∈ set_diff l l' <-> a ∈ l /\ a ∉ l'.
-Proof.
+Proof using H6 H5 H3 H2 H1 H0 EqDecision0.
   split.
   - by eauto using set_diff_elim1, set_diff_elim2.
   - by intros []; apply set_diff_intro.
diff --git a/theories/VLSM/Lib/StdppListSet.v b/theories/VLSM/Lib/StdppListSet.v
index ad3d8129..0f0c9384 100644
--- a/theories/VLSM/Lib/StdppListSet.v
+++ b/theories/VLSM/Lib/StdppListSet.v
@@ -1,6 +1,8 @@
 From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 
+Set Default Proof Using "Type".
+
 Section sec_fst_defs.
 
 Context `{EqDecision A}.
diff --git a/theories/VLSM/Lib/StreamExtras.v b/theories/VLSM/Lib/StreamExtras.v
index 775f33b0..34515d2d 100644
--- a/theories/VLSM/Lib/StreamExtras.v
+++ b/theories/VLSM/Lib/StreamExtras.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From Coq Require Import Streams Sorted.
 From VLSM.Lib Require Import Preamble ListExtras StdppExtras SortedLists NeList.
 
+Set Default Proof Using "Type".
+
 (** * Stream utility definitions and lemmas *)
 
 Lemma stream_eq_hd_tl {A} (s s' : Stream A) :
diff --git a/theories/VLSM/Lib/StreamFilters.v b/theories/VLSM/Lib/StreamFilters.v
index d1d629af..f4b110ff 100644
--- a/theories/VLSM/Lib/StreamFilters.v
+++ b/theories/VLSM/Lib/StreamFilters.v
@@ -2,6 +2,8 @@ From stdpp Require Import prelude.
 From Coq Require Import Streams Sorted.
 From VLSM.Lib Require Import Preamble StreamExtras SortedLists ListExtras StdppExtras NeList.
 
+Set Default Proof Using "Type".
+
 (**
   Given a predicate <<P>> and a stream <<s>>, a stream of naturals <<ns>>
   determines a [filtering_subsequence] for <<P>> on <<s>> if it corresponds to
@@ -377,7 +379,7 @@ Fixpoint stream_filter_fst_pos
   (n : nat)
   {struct Hev}
   : nat * Stream A.
-Proof.
+Proof using Pdec.
   refine
     (match decide (P (hd s)) with
       | left p => (n, tl s)
diff --git a/theories/VLSM/Lib/Temporal.v b/theories/VLSM/Lib/Temporal.v
index 9e01d251..5120be0e 100644
--- a/theories/VLSM/Lib/Temporal.v
+++ b/theories/VLSM/Lib/Temporal.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From Coq Require Import Streams Classical.
 
+Set Default Proof Using "Type".
+
 (** * Temporal Logic Predicates and Results *)
 
 Set Implicit Arguments.
diff --git a/theories/VLSM/Lib/TopSort.v b/theories/VLSM/Lib/TopSort.v
index 54bcf69d..d86f86ca 100644
--- a/theories/VLSM/Lib/TopSort.v
+++ b/theories/VLSM/Lib/TopSort.v
@@ -2,6 +2,8 @@ From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude.
 From VLSM.Lib Require Import Preamble ListExtras ListSetExtras StdppListSet StdppExtras.
 
+Set Default Proof Using "Type".
+
 (** * Topological sorting implementation
 
   This module implements an algorithm producing a linear extension for a
@@ -131,7 +133,7 @@ Lemma precedes_irreflexive
   (a : A)
   (Ha : P a)
   : ~ precedes a a.
-Proof.
+Proof using RelDecision0 Hso.
   specialize (StrictOrder_Irreflexive (exist P a Ha)).
   unfold complement; unfold precedes_P; simpl; intro Hirr.
   by destruct (decide (precedes a a)).
@@ -143,7 +145,7 @@ Lemma precedes_asymmetric
   (Hb : P b)
   (Hab : precedes a b)
   : ~ precedes b a.
-Proof.
+Proof using Hso.
   intro Hba.
   exact
     (StrictOrder_Asymmetric Hso
@@ -159,7 +161,7 @@ Lemma precedes_transitive
   (Hab : precedes a b)
   (Hbc : precedes b c)
   : precedes a c.
-Proof.
+Proof using Hso.
   exact
     (RelationClasses.StrictOrder_Transitive
       (exist P a Ha) (exist P b Hb) (exist P c Hc)
@@ -173,7 +175,7 @@ Qed.
 Lemma count_predecessors_zero
   (Hl : l <> [])
   : Exists (fun a => count_predecessors a = 0) l.
-Proof.
+Proof using P Hso HPl.
   unfold count_predecessors.
   induction l; [done |].
   inversion_clear HPl as [| ? ? HPa HPl0].
@@ -214,7 +216,7 @@ Lemma min_predecessors_zero
   (Hl : l = a :: l')
   (min := min_predecessors l' a)
   : count_predecessors min = 0.
-Proof.
+Proof using P Hso HPl.
   assert (Hl' : l <> []) by (intro H; rewrite Hl in H; inversion H).
   specialize (count_predecessors_zero Hl'); intro Hx.
   apply Exists_exists in Hx. destruct Hx as [x [Hinx Hcountx]].
@@ -300,7 +302,7 @@ Lemma topologically_sorted_occurrences_ordering
   (lb1 lb2 : list A)
   (Heqb : l = lb1 ++ [b] ++ lb2)
   : exists (lab : list A), lb1 = la1 ++ a :: lab.
-Proof.
+Proof using RelDecision0 P Hts Hso Hl.
   assert (Hpa : P a).
   { rewrite Forall_forall in Hl. apply Hl. rewrite Heqa, !elem_of_app, elem_of_list_singleton. auto. }
   specialize (Hts a b Hab lb1 lb2 Heqb).
@@ -325,7 +327,7 @@ Corollary top_sort_before
   (l1 l2 : list A)
   (Heq : l = l1 ++ [b] ++ l2)
   : a ∈ l1.
-Proof.
+Proof using RelDecision0 P Hts Hso Hl.
   apply elem_of_list_split in Ha.
   destruct Ha as [la1 [la2 Ha]].
   specialize (topologically_sorted_occurrences_ordering a b Hab la1 la2 Ha l1 l2 Heq).
@@ -343,7 +345,7 @@ Corollary top_sort_precedes
   (Ha : a ∈ l)
   (Hb : b ∈ l)
   : exists l1 l2 l3, l = l1 ++ [a] ++ l2 ++ [b] ++ l3.
-Proof.
+Proof using RelDecision0 P Hts Hso Hl.
   apply elem_of_list_split in Hb.
   destruct Hb as [l12 [l3 Hb']].
   specialize (top_sort_before a b Hab Ha l12 l3 Hb').
@@ -550,7 +552,7 @@ Context
   <<l>>, [top_sort] <<l>> is [topologically_sorted].
 *)
 Lemma top_sort_sorted : topologically_sorted precedes (top_sort l).
-Proof.
+Proof using P Hso Hl.
   intro a; intros.
   intro Ha2.
   assert (Ha : a ∈ l).
@@ -638,7 +640,7 @@ Definition topological_sorting
   set_eq l lts /\ topologically_sorted precedes lts.
 
 Corollary top_sort_correct : topological_sorting l (top_sort l).
-Proof.
+Proof using P Hso Hl.
   split.
   - by apply top_sort_set_eq.
   - by apply top_sort_sorted.
@@ -652,7 +654,7 @@ Lemma maximal_element_in
   (a : A)
   (Hmax : get_maximal_element = Some a) :
   a ∈ l.
-Proof.
+Proof using P Hso Hl.
   unfold get_maximal_element in Hmax.
   assert (exists l', l' ++ [a] = top_sort l).
   {
@@ -681,7 +683,7 @@ Lemma get_maximal_element_correct
   (Hina : a ∈ l)
   (Hmax : get_maximal_element = Some max) :
   ~ precedes max a.
-Proof.
+Proof using P Hso Hl.
   specialize top_sort_correct as [Hseteq Htop].
   unfold topologically_sorted in Htop.
   intros contra.
@@ -721,7 +723,7 @@ Qed.
 Lemma get_maximal_element_some
   (Hne : l <> []) :
   exists a, get_maximal_element = Some a.
-Proof.
+Proof using P Hl.
   unfold get_maximal_element.
   destruct l; cbn; [by congruence |].
   exists (List.last
@@ -762,14 +764,14 @@ Corollary simple_topologically_sorted_precedes_closed_remove_last
   (Hinit : l = init ++ [final])
   (Hpc : precedes_closed precedes l)
   : precedes_closed precedes init.
-Proof.
+Proof using StrictOrder0.
   by eapply topologically_sorted_precedes_closed_remove_last;
     [typeclasses eauto | apply Forall_True | ..].
 Qed.
 
 Corollary simple_top_sort_correct : forall l,
   topological_sorting precedes l (top_sort precedes l).
-Proof.
+Proof using StrictOrder0.
   by intro; eapply top_sort_correct; [typeclasses eauto | apply Forall_True].
 Qed.
 
@@ -777,7 +779,7 @@ Corollary simple_maximal_element_in l
   (a : A)
   (Hmax : get_maximal_element precedes l = Some a) :
   a ∈ l.
-Proof.
+Proof using StrictOrder0.
   by eapply maximal_element_in; [typeclasses eauto | apply Forall_True |].
 Qed.
 
@@ -786,7 +788,7 @@ Corollary simple_get_maximal_element_correct l
   (Hina : a ∈ l)
   (Hmax : get_maximal_element precedes l = Some max) :
   ~ precedes max a.
-Proof.
+Proof using StrictOrder0.
   by eapply get_maximal_element_correct; [typeclasses eauto | apply Forall_True | ..].
 Qed.
 
diff --git a/theories/VLSM/Lib/TraceClassicalProperties.v b/theories/VLSM/Lib/TraceClassicalProperties.v
index 806a4700..094dd60f 100644
--- a/theories/VLSM/Lib/TraceClassicalProperties.v
+++ b/theories/VLSM/Lib/TraceClassicalProperties.v
@@ -1,6 +1,7 @@
 From Coq Require Import Classical ClassicalEpsilon.
 From VLSM.Lib Require Import SsrExport Traces TraceProperties.
 
+Set Default Proof Using "Type".
 Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
diff --git a/theories/VLSM/Lib/TraceProperties.v b/theories/VLSM/Lib/TraceProperties.v
index ca9c6f68..4f20c408 100644
--- a/theories/VLSM/Lib/TraceProperties.v
+++ b/theories/VLSM/Lib/TraceProperties.v
@@ -1,6 +1,7 @@
 From Coq Require Import Program.Equality.
 From VLSM.Lib Require Import SsrExport Traces.
 
+Set Default Proof Using "Type".
 Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
diff --git a/theories/VLSM/Lib/Traces.v b/theories/VLSM/Lib/Traces.v
index 36593d41..8974682a 100644
--- a/theories/VLSM/Lib/Traces.v
+++ b/theories/VLSM/Lib/Traces.v
@@ -1,5 +1,6 @@
 From VLSM.Lib Require Import SsrExport.
 
+Set Default Proof Using "Type".
 Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.