Removal of another useless premise (map_config_merge)

CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v

@@ -342,7 +342,6 @@ apply (update_compat
   config); auto.
 + rewrite <- (map_config_id config) at 2. rewrite map_config_merge.
   - f_equiv. intros x y Hxy. simpl. now rewrite Bijection.retraction_section.
-  - auto.
   - simpl. repeat intro. now subst.
 + unfold lift_path; cbn -[straight_path isobarycenter].
   intro. now rewrite Bijection.retraction_section, Hda.

CaseStudies/Gathering/InR2/Peleg.v

@@ -362,7 +362,6 @@ apply get_location_compat, update_compat; auto.
                                      (lift (existT precondition (frame_choice_bijection sim)
                                            (precondition_satisfied da config g)) x))); try reflexivity; [].
     rewrite 2 get_location_lift. simpl. rewrite Bijection.retraction_section. apply Hxy.
-  - autoclass.
   - apply lift_compat. intros x y Hxy. now rewrite Hxy.
 + 
 Admitted. (* Peleg's gathering in FSYNC: round_simplify -> hypothesis missing on the demon *)

Core/Configuration.v

@@ -177,7 +177,7 @@ Lemma map_config_id `{State} `{Names} : forall config,
 Proof using . now repeat intro. Qed.
 
 Lemma map_config_merge `{Location} {T U V : Type} `{@State _ T} `{@State _ U} `{@State _ V} `{Names} :
-  forall (f : T -> U) (g : U -> V), Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) g ->
+  forall (f : T -> U) (g : U -> V), Proper (equiv ==> equiv) g ->
   forall config : configuration, map_config g (map_config f config) == map_config (fun x => g (f x)) config.
 Proof using . now repeat intro. Qed.