diff --git a/CaseStudies/Exploration/ExplorationDefs.v b/CaseStudies/Exploration/ExplorationDefs.v
index 964f5a4b8df146f970add99fba9f82f67daa0f04..0229171cbc4ad13e37329da963cecaf786eb99cf 100644
--- a/CaseStudies/Exploration/ExplorationDefs.v
+++ b/CaseStudies/Exploration/ExplorationDefs.v
@@ -22,6 +22,12 @@ Definition is_visited (l : location) (c : configuration) : Prop :=
 Definition Will_be_visited (l : location) (e : execution) : Prop :=
   eventually (instant (is_visited l)) e.
 
+Definition simple_exploration (e : execution) :=
+  forall pt, Will_be_visited pt e.
+
+Definition perpetual_exploration (e : execution) :=
+  Stream.forever simple_exploration e.
+
 (** Eventually, all robots stop moving. *)
 Definition Stall (e : execution) := hd e == (hd (tl e)).
 
@@ -34,7 +40,7 @@ Definition Will_stop (e : execution) : Prop :=
 (** [ExplorationStop e] means that after a finite time, every node of the space has been
   visited, and after that time, all robots will stay at the same place forever. *)
 Definition ExplorationStop (e : execution) :=
-  (forall l, Will_be_visited l e) /\ Will_stop e.
+  simple_exploration e /\ Will_stop e.
 
 Global Instance is_visited_compat :
   Proper (equiv ==> equiv ==> iff) is_visited.
@@ -52,6 +58,16 @@ Proof using .
   - rewrite He, Hl. exact H.
 Qed.
 
+Global Instance simple_exploration_compat :
+  Proper (equiv ==> iff) simple_exploration.
+Proof using .
+  intros e1 e2 He. unfold simple_exploration. now setoid_rewrite He.
+Qed.
+
+Global Instance perpetual_exploration_compat :
+  Proper (equiv ==> iff) perpetual_exploration.
+Proof using . apply Stream.forever_compat, simple_exploration_compat. Qed.
+
 Global Instance Stall_compat : Proper (equiv ==> iff) Stall.
 Proof using .
   intros e1 e2 He. unfold Stall. split; intros H.
@@ -85,5 +101,4 @@ Proof using .
     + rewrite He. exact Hs.
 Qed.
 
-
 End ExplorationDefs.