proposition: Theorem compMap_fission_ex : forall (A : Type)(B C : Set)(eqdb : EqDec B)(eqdc : EqDec C) (c1 : A -> Comp B)(c2 : B -> Comp C)(ls : list A), comp_spec eq (compMap _ (fun a => b <-$ c1 a; c2 b) ls) (ls' <-$ compMap _ c1 ls; compMap _ c2 ls').
proof: Proof. induction ls; intuition; simpl in *. comp_simp; simpl; reflexivity. inline_first; comp_skip; inline_first. comp_swap_l. eapply comp_spec_eq_trans. eapply (@comp_spec_seq (list C) (list C)); eauto with inhabited. intuition; subst. eapply comp_spec_eq_refl. inline_first; comp_skip; comp_simp; simpl. comp_swap_r; comp_skip. Qed.
imports: FCF.FCF Permutation