Apply suggestions from code review

Co-authored-by: Wojciech Kołowski <wkolowski@protonmail.com>

Author: traiansf

theories/VLSM/Core/ByzantineTraces/FixedSetByzantineTraces.v

@@ -300,7 +300,7 @@ Lemma fixed_non_byzantine_projection_incl_preloaded
 Proof.
   apply basic_VLSM_strong_incl.
   - intros is. apply fixed_non_byzantine_projection_initial_state_preservation.
-  - intros m Hm. exact I.
+  - intros m Hm. compute. trivial.
   - intros l s om Hv.
     split; [|exact I].
     revert Hv.

theories/VLSM/Core/SubProjectionTraces.v

@@ -390,14 +390,12 @@ Lemma induced_sub_projection_preloaded_free_incl
   : VLSM_incl induced_sub_projection (pre_loaded_with_all_messages_vlsm (free_composite_vlsm sub_IM)).
 Proof.
   apply basic_VLSM_strong_incl.
-  2: cbv; intuition.
   - intros s (sX & <- & HsX) sub_i.
     destruct_dec_sig sub_i i Hi Heqsub_i.
-    subst.
-    apply (HsX i).
+    subst. apply HsX.
+  - cbv; intuition.
   - intros (sub_i, li) s om Hv.
-    split; [|exact I].
-    cbn.
+    split; [cbn |exact I].
     destruct_dec_sig sub_i i Hi Heqsub_i; subst.
     apply induced_sub_projection_valid_projection_strong.
     assumption.

theories/VLSM/Lib/ListExtras.v

@@ -4,19 +4,16 @@ From VLSM Require Import Lib.Preamble.
 
 (** * Utility lemmas about lists *)
 
-Lemma map_composed
+Lemma map_comp
   [A B C : Type]
   (f : A -> B)
   (g : B -> C)
   : map (g ∘ f) = map g ∘ map f.
 Proof.
   extensionality l.
-  induction l; [reflexivity|]; cbn.
-  rewrite IHl.
-  reflexivity.
+  induction l; cbn; rewrite ?IHl; reflexivity.
 Qed.
 
-
 (** A list is empty if it has no members *)
 Lemma empty_nil [X:Type] (l:list X) :
   (forall v, ~In v l) -> l = [].
@@ -1281,20 +1278,15 @@ Definition map_option
     )
     [].
 
-Lemma map_option_composed_right
-  [A B C : Type]
-  (f : A -> B)
-  (g : B -> option C)
-  : map_option (g ∘ f) = map_option g ∘ map f.
+Lemma map_option_comp_r
+  [A B C : Type] (f : A -> B) (g : B -> option C) :
+    map_option (g ∘ f) = map_option g ∘ map f.
 Proof.
   extensionality l.
-  induction l; [reflexivity|].
-  cbn.
-  rewrite IHl.
-  reflexivity.
+  induction l; cbn; rewrite ?IHl; reflexivity.
 Qed.
 
-Lemma map_option_composed_left
+Lemma map_option_comp_l
   [A B C : Type]
   (f : A -> option B)
   (g : B -> C)