proof step with incorrect env give same trace

src/syntax/FlightPlanSized.v

@@ -32,7 +32,8 @@ Set Implicit Arguments.
 Definition correct_block_id (fp: flight_plan) (id: block_id): Prop :=
   (id < get_nb_block fp).
 
-Lemma normalise_block_id_is_correct : forall (fp: flight_plan) (id: block_id),
+Lemma normalise_block_id_is_correct : 
+  forall (fp: flight_plan) (id: block_id),
   correct_block_id fp (normalise_block_id fp id).
 Proof.
   intros fp id. unfold normalise_block_id.