diff --git a/searchAndDestroy.sh b/searchAndDestroy.sh
index d609e7a1..b8684358 100755
--- a/searchAndDestroy.sh
+++ b/searchAndDestroy.sh
@@ -1,4 +1,4 @@
-for file in `find theories/VLSM/Core/ELMO/ -maxdepth 1 -name 'UMO.v'`; do 
+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
diff --git a/theories/VLSM/Core/ELMO/BaseELMO.v b/theories/VLSM/Core/ELMO/BaseELMO.v
index 4cb116c8..2e487627 100644
--- a/theories/VLSM/Core/ELMO/BaseELMO.v
+++ b/theories/VLSM/Core/ELMO/BaseELMO.v
@@ -1,3 +1,4 @@
+Set Default Proof Using "Type".
 From VLSM.Lib Require Import Itauto.
 From stdpp Require Import prelude finite.
 From VLSM.Lib Require Import EquationsExtras.
diff --git a/theories/VLSM/Core/ELMO/ELMO.v b/theories/VLSM/Core/ELMO/ELMO.v
index 0db2eb61..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.
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.