proposition: Lemma compMap_map : forall (A: Type)(B : Set)(eqd : EqDec B)(f : A -> B) ls, comp_spec eq (compMap _ (fun a => ret (f a)) ls) (ret (map f ls)).
proof: Proof. induction ls; intuition. simpl. eapply comp_spec_eq_refl. simpl. prog_simp. eapply comp_spec_eq_trans. eapply comp_spec_seq_eq; intuition. eapply IHls. eapply comp_spec_eq_refl. prog_simp. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF