proposition: Theorem fold_map_fission_spec : forall (A E : Set)(P : A -> E -> Prop)(B : Type)(D : Set)(eqdA : EqDec A)(c1 : A -> B -> Comp A)(ls_b : list B)(init_a : A) (eqdD : EqDec D)(eqdE : EqDec E)(c2 : B -> Comp D)(c3 : E -> D -> Comp E)(init_e : E), P init_a init_e -> (forall a b e, P a e -> comp_spec P (c1 a b) (a0 <-$ c2 b; c3 e a0)) -> comp_spec P (compFold _ c1 init_a ls_b) (ls_d <-$ (compMap _ c2 ls_b); compFold _ c3 init_e ls_d).
proof: Proof. induction ls_b; intuition. simpl. prog_simp. simpl. eapply comp_spec_ret. trivial. 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. Ltac prog_assoc_r := eapply comp_spec_eq_trans_r; [ idtac | eapply comp_spec_assoc]. prog_assoc_r. eapply comp_spec_seq; intuition. Qed.
imports: FCF.FCF