diff --git a/CaseStudies/Convergence/Algorithm_noB_Assumptions.v b/CaseStudies/Convergence/Algorithm_noB_Assumptions.v
new file mode 100644
index 0000000000000000000000000000000000000000..032595be1300d9e302644b87c1be9a0daefc5b63
--- /dev/null
+++ b/CaseStudies/Convergence/Algorithm_noB_Assumptions.v
@@ -0,0 +1,2 @@
+Require Pactole.CaseStudies.Convergence.Algorithm_noB.
+Print Assumptions Algorithm_noB.convergence_FSYNC.
diff --git a/CaseStudies/Gathering/InR2/Algorithm_withLight.v b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
index 70bdd2b24c9b28ec21c4c7521ba5a32df7d4cd49..10f19d4a0622a3f89a989b7c09ce5d999491e39a 100644
--- a/CaseStudies/Gathering/InR2/Algorithm_withLight.v
+++ b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
@@ -7039,7 +7039,7 @@ Qed.
 
 (** The final theorem. *)
 Theorem Gathering_in_R2 : forall d : similarity_demon,
- SSYNC (d : demon) -> Fair d -> ValidSolGathering gatherR2 d.
+ SSYNC (d : demon) -> Fair d -> FullSolGathering gatherR2 d.
 Proof using .
 intro d. generalize (similarity_demon2prop d).
 generalize (similarity_demon2demon d). clear d.
diff --git a/CaseStudies/Gathering/WithMultiplicityLight.v b/CaseStudies/Gathering/WithMultiplicityLight.v
index 9c31669affcdfbf1ff0eebcf32249b5f6ed60491..1bb092f2767704a6604ad806fe25d89ade81ad23 100644
--- a/CaseStudies/Gathering/WithMultiplicityLight.v
+++ b/CaseStudies/Gathering/WithMultiplicityLight.v
@@ -31,8 +31,6 @@ Set Implicit Arguments.
 Typeclasses eauto := (bfs) 5.
 Require Even.
 
-(* Local Existing Instance Pactole.Util.FMaps.FMapInterface.prod_Setoid. *)
-(* Local Existing Instance Pactole.Util.FMaps.FMapInterface.prod_EqDec. *)
 Local Existing Instance fst_compat_pactole.
 Local Existing Instance snd_compat_pactole.
 Local Existing Instance pair_compat_pactole.
@@ -127,14 +125,7 @@ Qed.
 
 Existing Instance eqlistA_Setoid.
 Existing Instance eqlistA_EqDec.
-(*
-Record obsLight := {
-    fst_lght: list nat;         (* todo: rename into oberver_light_column *)
-    snd_lght: list nat;         (* other_light_column *)
-    observer_lght: L;           (* color of the observing robot *)
-    is_on_max_black: bool       (* is the observing robot on max black column? *)
-  }.
-*)
+
 Record obsLight := {
     observer_lght: L;           (* color of the observing robot *)
     colors: multiset (location*L);
@@ -286,9 +277,6 @@ Lemma cardinal_fst_obs_from_config : forall config state,
   cardinal (fst (obs_from_config (Observation:=Obs) config state)) = nG + nB.
 Proof. intros. cbn -[make_multiset cardinal nB nG location]. apply cardinal_obs_from_config. Qed.
 
-(* Lemma obs_from_config_ignore_snd : nG <> 0 -> forall (ref_st : location * L) config st, *)
-  (* fst (obs_from_config (Observation := Obs) config st) == fst (obs_from_config config ref_st). *)
-
 Lemma obs_from_config_ignore_snd_except_observerlight :
   forall (ref_st : location * L) config st,
   let o := obs_from_config config ref_st in
@@ -625,24 +613,6 @@ rewrite Hl in Hlgth.
 cbn in *. lia.
 Qed.
 
-(* We need to unfold [obs_is_ok] for rewriting *)
-(*
-Lemma obs_from_config_snd_spec : forall (config : configuration) st (pt : location) (col:L),
-  (colors (snd (!!! (config,st))))[(pt,col)] =
-    countA_occ _ (fun id : ident => andb (get_light_decb config col id) (if (get_location (config id)) =?= (pt,col) then true else false)) col (config_list config).
-Proof. intros. now destruct (obs_from_config_spec config (pt, witness)) as [Hok _]. Qed.
-
-Lemma obs_non_nil : 2 <= nG+nB -> forall config st,
-  fst (!!! (config,st)) =/= MMultisetInterface.empty.
-Proof using .
-simpl obs_from_config. intros HnG config st Heq.
-assert (Hlgth:= config_list_length config).
-assert (Hl : config_list config = nil).
-{ apply (map_eq_nil fst). rewrite <- make_multiset_empty. apply Heq. }
-rewrite Hl in Hlgth.
-cbn in *. lia.
-Qed.
-*)
 Local Instance obs_compat : forall pt,
   Proper (equiv ==> eq) (fun obs : location * L => if fst obs =?= pt then true else false).
 Proof.
@@ -1354,33 +1324,6 @@ Proof.
   destruct (support (!! c)) as [ | x [ | y [ | z l] ]] eqn:heq_supp; try now (exfalso; cbn in h_size;lia).
   eauto.
 Qed.
-(*
-Lemma l_list_all_colors: 
-  ∀ x : L,
-    List.In x l_list
-    → (colors (snd (!!! (c, (0%VS, witness)))))[(pt1, x)] =
-        (colors (snd (!!! (c, (0%VS, witness)))))[(pt2, x)]
-    -> (∀ x : L,
-         ∃ x', x == x' /\ 
-                 (colors (snd (!!! (c, (0%VS, witness)))))[(pt1, x')] =
-                   (colors (snd (!!! (c, (0%VS, witness)))))[(pt2, x')]).
-Proof.
-  { intros x. 
-    specialize (@InA_alt L equiv) as h.
-    let ll := l_list in specialize h with (l:=ll).
-    assert ( ∀ x : L, (∃ y : L, x == y ∧ List.In y l_list)) as h_ex.
-    { intros x0.
-      rewrite <- h.
-      apply L_list_InA. }
-    specialize (h_ex x).
-    destruct h_ex as [ y [h_xy h_in]].
-    exists y;auto. }
-      
-.
-Proof.
-  
-Qed.
-*)
 
 Lemma colors_indep:
   forall c st st',
@@ -1594,10 +1537,6 @@ destruct (color_bivalent_obs (!!! (config, (origin, witness)))) eqn:Hcase.
 Qed.
 
 
-Definition ValidSolGathering (r : robogram) (d : demon) :=
-  forall config : configuration, WillGather (execute r d config).
-
-
 Lemma bivalent_sim : forall (sim : similarity location) Psim obs,
   bivalent (map_config (lift (existT precondition sim Psim)) obs) <-> bivalent obs.
 Proof.
diff --git a/Models/GraphEquivalence.v b/Models/GraphEquivalence.v
index 014a8076e73861d47243e8f4c0936adaa29036c2..6ddf64f48a67e4dbfe742e49d6118feb5b7478ee 100644
--- a/Models/GraphEquivalence.v
+++ b/Models/GraphEquivalence.v
@@ -305,7 +305,7 @@ try destruct (v1 =?= src target1) as [Hsrc1 | Hsrc1],
 + tauto.
 Defined.
 
-Theorem graph_equivD2C : forall (config : DGF_config) (rbg : robogramV) (da : DGF_da),
+Theorem graph_equiv_D2C : forall (config : DGF_config) (rbg : robogramV) (da : DGF_da),
   config_V2G (round rbg da config) == round (rbg_V2G rbg) (da_D2C da) (config_V2G config).
 Proof using All.
 intros config rbg da id.
diff --git a/Models/GraphEquivalence_Assumptions.v b/Models/GraphEquivalence_Assumptions.v
new file mode 100644
index 0000000000000000000000000000000000000000..2b85155129b99a181056d3a5ee09b4780cb84660
--- /dev/null
+++ b/Models/GraphEquivalence_Assumptions.v
@@ -0,0 +1,4 @@
+From Pactole Require GraphEquivalence.
+
+Print Assumptions GraphEquivalence.graph_equiv_D2C.
+Print Assumptions GraphEquivalence.graph_equiv_C2D.
diff --git a/_CoqProject b/_CoqProject
index 53169a93c192a3a6f20ff17c6e7b8517e0819860..883c93a7160ca697340f5f5dd3b4c09ff6cb1d2c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,6 +8,8 @@
 # <8.12. We only support >= 8.12 now so this is nont needed anymore.
 -arg -w
 -arg -deprecated-hint-without-locality
+-arg -w
+-arg -deprecated-instance-without-locality
 
 # Spaces in args are not supported, see Makefile.local
 #-arg -set
@@ -51,13 +53,14 @@ Setting.v
 Models/NoByzantine.v
 Models/Flexible.v
 Models/Rigid.v
-Models/RigidFlexibleEquivalence.v
-Models/RigidFlexibleEquivalence_Assumptions.v
 Models/DiscreteGraph.v
 Models/Isometry.v
 Models/Similarity.v
 Models/ContinuousGraph.v
+Models/RigidFlexibleEquivalence.v
+Models/RigidFlexibleEquivalence_Assumptions.v
 Models/GraphEquivalence.v
+Models/GraphEquivalence_Assumptions.v
 
 ## Spaces
 Spaces/RealVectorSpace.v
diff --git a/dev/build_package.sh b/dev/build_package.sh
index ff3060a9fb6e6d549d8e1cf33c0798d16487a461..33d6dec3f2488c32f7320e6534c7de63c7f73b64 100755
--- a/dev/build_package.sh
+++ b/dev/build_package.sh
@@ -19,42 +19,134 @@ mkdir ./package/CaseStudies/Gathering
 mkdir ./package/CaseStudies/Gathering/InR
 mkdir ./package/CaseStudies/Gathering/InR2
 mkdir ./package/CaseStudies/Exploration
+mkdir ./package/CaseStudies/LifeLine
+mkdir ./package/minipactole
 
 # Create a fresh Makefile from the _CoqPoject
 coq_makefile -f _CoqProject -o Makefile
 
 # Copy files into each directory
-cp Util/FSets/FSetInterface.v Util/FSets/FSetFacts.v Util/FSets/FSetList.v ./package/Util/FSets/
-
-cp Util/FMaps/FMapInterface.v Util/FMaps/FMapFacts.v Util/FMaps/FMapList.v ./package/Util/FMaps/
-
-cp Util/MMultiset/Preliminary.v Util/MMultiset/MMultisetInterface.v Util/MMultiset/MMultisetFacts.v Util/MMultiset/MMultisetWMap.v Util/MMultiset/MMultisetExtraOps.v ./package/Util/MMultiset/
-
-cp Util/Coqlib.v Util/Preliminary.v Util/SetoidDefs.v Util/NumberComplements.v Util/ListComplements.v Util/Ratio.v Util/Lexprod.v Util/Stream.v Util/Bijection.v ./package/Util/
-
-cp Core/Robots.v Core/RobotInfo.v Core/Configurations.v Core/Formalism.v ./package/Core/
-
-cp Setting.v Makefile _CoqProject ./package/
-
-cp Spaces/RealVectorSpace.v Spaces/RealMetricSpace.v Spaces/RealNormedSpace.v Spaces/EuclideanSpace.v Spaces/Similarity.v Spaces/R.v Spaces/R2.v Spaces/Graph.v Spaces/Ring.v Spaces/Grid.v Spaces/Isomorphism.v ./package/Spaces/
-
-cp Observations/Definition.v Observations/MultisetObservation.v Observations/SetObservation.v Observations/LimitedMultisetObservation.v Observations/LimitedSetObservation.v ./package/Observations/
-
-cp Models/Rigid.v Models/Flexible.v Models/Similarity.v Models/RigidFlexibleEquivalence.v Models/DiscreteGraph.v Models/ContinuousGraph.v Models/GraphEquivalence.v ./package/Models/
-
-cp CaseStudies/Convergence/Impossibility_2G_1B.v CaseStudies/Convergence/Algorithm_noB.v ./package/CaseStudies/Convergence/
-
-cp CaseStudies/Gathering/Definitions.v CaseStudies/Gathering/WithMultiplicity.v CaseStudies/Gathering/Impossibility.v ./package/CaseStudies/Gathering/
-
-cp CaseStudies/Gathering/InR/Algorithm.v CaseStudies/Gathering/InR/Impossibility.v ./package/CaseStudies/Gathering/InR/
-
-cp CaseStudies/Gathering/InR2/Algorithm.v ./package/CaseStudies/Gathering/InR2/
-#Gathering/InR2/FSyncFlexNoMultAlgorithm.v Gathering/InR2/Peleg.v
-
-cp CaseStudies/Exploration/Definitions.v CaseStudies/Exploration/ImpossibilityKDividesN.v CaseStudies/Exploration/Tower.v ./package/CaseStudies/Exploration/
-
-# Specific to workshops/lectures
-cp exercises.v ./package/
+cp Util/FSets/FSetInterface.v \
+   Util/FSets/FSetFacts.v \
+   Util/FSets/FSetList.v \
+   ./package/Util/FSets/
+
+cp Util/FMaps/FMapInterface.v \
+   Util/FMaps/FMapFacts.v \
+   Util/FMaps/FMapList.v \
+   ./package/Util/FMaps/
+
+cp Util/MMultiset/Preliminary.v \
+   Util/MMultiset/MMultisetInterface.v \
+   Util/MMultiset/MMultisetFacts.v \
+   Util/MMultiset/MMultisetWMap.v \
+   Util/MMultiset/MMultisetExtraOps.v \
+   ./package/Util/MMultiset/
+
+cp Util/Coqlib.v \
+   Util/Preliminary.v \
+   Util/SetoidDefs.v \
+   Util/NumberComplements.v \
+   Util/ListComplements.v \
+   Util/Ratio.v \
+   Util/Lexprod.v \
+   Util/Stream.v \
+   Util/Bijection.v \
+   ./package/Util/
+
+cp Core/Identifiers.v \
+   Core/State.v \
+   Core/Configuration.v \
+   Core/Formalism.v \
+   ./package/Core/
+
+cp Setting.v \
+   Pactole_all.v \
+   Makefile \
+   _CoqProject \
+   ./package/
+
+cp Spaces/RealVectorSpace.v \
+   Spaces/RealMetricSpace.v \
+   Spaces/RealNormedSpace.v \
+   Spaces/EuclideanSpace.v \
+   Spaces/Similarity.v \
+   Spaces/Isometry.v \
+   Spaces/R.v \
+   Spaces/R2.v \
+   Spaces/Graph.v \
+   Spaces/Ring.v \
+   Spaces/Grid.v \
+   Spaces/Isomorphism.v \
+   ./package/Spaces/
+
+cp Observations/Definition.v \
+   Observations/MultisetObservation.v \
+   Observations/MultisetObservationInfo.v \
+   Observations/SetObservation.v \
+   Observations/LimitedMultisetObservation.v \
+   Observations/LimitedSetObservation.v \
+   Observations/PointedObservation.v \
+   Observations/PreCompositionObservation.v \
+   Observations/PairObservation.v \
+   ./package/Observations/
+
+cp Models/NoByzantine.v \
+   Models/Rigid.v \
+   Models/Flexible.v \
+   Models/Isometry.v \
+   Models/Similarity.v \
+   Models/RigidFlexibleEquivalence.v \
+   Models/RigidFlexibleEquivalence_Assumptions.v \
+   Models/DiscreteGraph.v \
+   Models/ContinuousGraph.v \
+   Models/GraphEquivalence.v \
+   Models/GraphEquivalence_Assumptions.v \
+   ./package/Models/
+
+cp CaseStudies/Convergence/Impossibility_2G_1B.v \
+   CaseStudies/Convergence/Impossibility_2G_1B_Assumptions.v \
+   CaseStudies/Convergence/Algorithm_noB.v \
+   CaseStudies/Convergence/Algorithm_noB_Assumptions.v \
+   ./package/CaseStudies/Convergence/
+
+cp CaseStudies/Gathering/Definitions.v \
+   CaseStudies/Gathering/WithMultiplicity.v \
+   CaseStudies/Gathering/WithMultiplicityLight.v \
+   CaseStudies/Gathering/Impossibility.v \
+   CaseStudies/Gathering/Impossibility_Assumptions.v \
+   ./package/CaseStudies/Gathering/
+
+cp CaseStudies/Gathering/InR/Algorithm.v \
+   CaseStudies/Gathering/InR/Algorithm_Assumptions.v \
+   CaseStudies/Gathering/InR/Impossibility.v \
+   CaseStudies/Gathering/InR/Impossibility_Assumptions.v \
+   ./package/CaseStudies/Gathering/InR/
+
+cp CaseStudies/Gathering/InR2/Algorithm.v \
+   CaseStudies/Gathering/InR2/Algorithm_Assumptions.v \
+   CaseStudies/Gathering/InR2/Algorithm_withLight.v \
+   CaseStudies/Gathering/InR2/Algorithm_withLight_Assumptions.v \
+   CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v \
+   CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm_Assumptions.v \
+   CaseStudies/Gathering/InR2/Peleg.v \
+   CaseStudies/Gathering/InR2/Peleg_Assumptions.v \
+   CaseStudies/Gathering/InR2/Viglietta.v \
+   CaseStudies/Gathering/InR2/Viglietta_Assumptions.v \
+   ./package/CaseStudies/Gathering/InR2/
+
+cp CaseStudies/Exploration/Definitions.v \
+   CaseStudies/Exploration/ImpossibilityKDividesN.v \
+   CaseStudies/Exploration/ImpossibilityKDividesN_Assumptions.v \
+   CaseStudies/Exploration/Tower.v \
+   CaseStudies/Exploration/Tower_Assumptions.v \
+   ./package/CaseStudies/Exploration/
+
+cp CaseStudies/LifeLine/Algorithm.v \
+   ./package/CaseStudies/LifeLine/
+
+cp minipactole/minipactole.v \
+   ./package/minipactole/
 
 # Compile the archive to make sure it works
 time make -C package -j 3