diff --git a/src/utils.v b/src/utils.v index 32e4c8230d1d380d193efdce7a20cd14d982d158..f8244f17f168b773a6b850b9c6441601c0874af3 100644 --- a/src/utils.v +++ b/src/utils.v @@ -9,9 +9,7 @@ Proof. induction l. - reflexivity. - simpl. - destruct f. - + discriminate. - + exact IHl. + now destruct f. Qed. Lemma nth_error_on_composed_list : @@ -26,8 +24,7 @@ Proof. simpl. lia. - - rewrite (nth_error_nth' _ d Hlength), Hl, Hi, nth_middle. - reflexivity. + - now rewrite (nth_error_nth' _ d Hlength), Hl, Hi, nth_middle. Qed. Lemma map_in_the_middle : @@ -36,13 +33,7 @@ Lemma map_in_the_middle : List.nth_error (List.map f l) i = Some (f a). Proof. intros A B a d f l lpre lpost i Hl Hi. - - assert (List.nth_error l i = Some a) as Hnth. - apply (nth_error_on_composed_list _ _ d _ lpre lpost); - assumption. - - rewrite (map_nth_error _ i l Hnth). - reflexivity. + now apply map_nth_error, (nth_error_on_composed_list _ _ d _ lpre lpost). Qed. Section ListCustomBool.