diff --git a/CaseStudies/Gathering/InR2/Algorithm_withLight.v b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
index 5f696f2bb183508b83a580555ba893733b55784c..924ef899c4a0860bc58509f8185878d884628470 100644
--- a/CaseStudies/Gathering/InR2/Algorithm_withLight.v
+++ b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
@@ -7095,78 +7095,8 @@ destruct (gathered_at_dec config (get_location (config (Good g1)))) as [Hmove |
     - now destruct Hfair.
 Qed.
 
-(* *********** UNFAIR DEMON ************** *)
-
-(* Unfairness in terms of gathering: someone always moves if robots
-   are not gathered (and position is valid). *)
-Definition unfair_da_gathering r da config :=
-    (forall pt, ~gathered_at pt config) ->
-    changing r da config <> nil.
-
-Definition unfair_gathering r d config :=
-  Stream.forever2 (Stream.instant2 (unfair_da_gathering r)) d (execute r d config).
-
-(* We link this definition to the usual notion of unfairness:
-   if a robot can move, then some robot moves. *)
-
-Definition sim_da_with_all_activated da : similarity_da.
-Proof using .
-exists (da_with_all_activated da).
-apply (proj2_sig da).
-Defined.
-
-Lemma unfair_da_gather_impl: forall da config,
-    unfair_da gatherR2 (proj_sim_da da) config ->
-    unfair_da_gathering gatherR2 da config.
-Proof using .
-unfold unfair_da, unfair_da_gathering.
-intros da config Hunfair Hgather.
-apply Hunfair.
-destruct (OneMustChange (Good g1) (Hgather (get_location (config (Good g1)))))
-  as [gmove Hgmove].
-assert (Hall : List.In gmove (active (proj_sim_da (sim_da_with_all_activated da)))).
-{ unfold active. simpl. rewrite List.filter_In. auto using In_names. }
-specialize (Hgmove (sim_da_with_all_activated da)
-                   (FSYNC_SSYNC_da (da_with_all_activated_FSYNC_da da)) Hall).
-rewrite changing_spec in Hgmove.
-intro Habs. apply no_changing_same_config in Habs. apply Hgmove, Habs.
-Qed.
-
-Lemma unfair_gather_impl : forall d config,
-  unfair gatherR2 (similarity_demon2demon d) config ->
-  unfair_gathering gatherR2 d config.
-Proof using .
-coinduction cfsd.
-+ destruct H. clear -H. simpl in *. now apply unfair_da_gather_impl.
-+ now destruct H.
-Qed.
-
-(* Final theorem for unfair demons. *)
-Theorem unfair_Gathering_in_R2 : forall (d : similarity_demon) config,
-  SSYNC (d : demon) ->
-  unfair gatherR2 (d : demon) config ->
-  WillGather (execute gatherR2 d config).
-Proof using .
-intros d config Hssync Hunfair'.
-assert (Hunfair : unfair_gathering gatherR2 d config) by now apply unfair_gather_impl.
-clear Hunfair'.
-revert d Hssync Hunfair. pattern config.
-apply (well_founded_ind wf_lt_config). clear config.
-intros config Hind d Hssync Hunfair.
-(* Are we already gathered? *)
-destruct (gathered_at_dec config (get_location (config (Good g1)))) as [Hmove | Hmove].
-+ (* If so, not much to do *)
-  apply Stream.Now. exists (get_location (config (Good g1))). now apply gathered_at_OK.
-+ (* Otherwise, by assumption on the demon, a robot should move
-     so we can use our well-founded induction hypothesis. *)
-  destruct Hunfair as [Hactive Hunfair], Hssync. hnf in Hactive.
-  apply Stream.Later, Hind; trivial; try (now apply never_bivalent); [].
-  apply round_lt_config; trivial; [].
-  apply Hactive; trivial; []. intros pt Habs. apply Hmove. eapply gathered_precise, Habs.
-Qed.
 
 End GatheringInR2.
 
-(* this is ignored when coq -vos is used. This will fail when coqtop
-   if relying on .vos. But it will succeed when using .vo *)
+(* We prefer calling this from another file, see Algorithm_withLight_ASsumptions.v. *)
 (* Print Assumptions Gathering_in_R2. *)