proposition: Theorem compMap_seq_map : forall (A B: Type)(C : Set)(eqdc : EqDec C)(ls : list A)(f : A -> B)(c : B -> Comp C), comp_spec eq (compMap _ c (map f ls)) (compMap _ (fun x => c (f x)) ls).
proof: Proof. induction ls; intuition; simpl in *. eapply comp_spec_eq_refl. comp_skip. comp_skip. Qed.
imports: FCF.FCF Permutation