proposition: Theorem fold_map_fission_spec_eq : forall (A : Type)(B C: Set)(eqdB : EqDec B)(eqdC : EqDec C) ls c init (ca : A -> Comp B) cb, (forall a init, comp_spec eq (c init a) (x <-$ ca a; cb init x)) -> comp_spec eq (compFold _ c init ls) (lsa <-$ (compMap _ ca ls); compFold _ cb init lsa).
proof: Proof. induction ls; intuition. unfold compMap. prog_simp. eapply comp_spec_eq_refl. simpl. prog_inline_first. prog_at prog_inline rightc 1%nat. simpl. prog_at prog_ret rightc 2. simpl. prog_at prog_swap rightc 1%nat. eapply comp_spec_eq_trans. eapply comp_spec_seq_eq; intuition. eapply comp_spec_eq_refl. prog_inline_first. do 2 prog_skip. Qed.
imports: FCF.FCF