proposition: Lemma compMap_flatten : forall (A: Type)(B : Set)(eqd : EqDec B)(c : A -> Comp B)(ls : list (list A)), comp_spec (fun ls1 ls2 => ls2 = flatten ls1) (compMap _ (fun ls' => compMap _ c ls') ls) (compMap _ c (flatten ls)).
proof: Proof. induction ls; intuition; simpl in *. eapply comp_spec_ret; simpl; intuition. eapply comp_spec_eq_trans_r. 2:{ eapply comp_spec_eq_symm. eapply eq_impl_comp_spec_eq. intros. eapply compMap_app. } comp_skip. eapply comp_spec_seq. apply nil. apply nil. eapply IHls. intuition. subst. eapply comp_spec_ret. simpl. intuition. Qed.
imports: FCF.FCF Permutation