proposition: Theorem compMap_fission_eq: forall (A : Type)(B C D : Set){eqdb : EqDec B}{eqdd : EqDec D}{eqdc : EqDec C}(ls : list A)(f1 : A -> Comp B)(f2 : A -> Comp C)(f3 : list B -> Comp (list D))(f4 : C -> Comp D) P, (comp_spec eq (f3 nil) (ret nil)) -> (forall a, comp_spec P (f1 a) (f2 a)) -> (forall r1 r2 r3, P r1 r2 -> comp_spec eq (f3 (r1 :: r3)) (r0 <-$ f3 r3; a0 <-$ f4 r2; ret a0 :: r0)) -> comp_spec eq (lsb <-$ compMap _ f1 ls; f3 lsb) (compMap _ (fun a => b <-$ f2 a; f4 b) ls).
proof: Proof. induction ls; intuition. unfold compMap. prog_simp. intuition. simpl. prog_inline_first. eapply comp_spec_seq; intuition; eauto with inhabited. eapply comp_spec_eq_trans. 2:{ eapply comp_spec_seq_eq; eauto with inhabited. eapply comp_spec_eq_refl. intuition. eapply comp_spec_seq_eq; eauto with inhabited. intuition. eapply comp_spec_eq_refl. } prog_swap_r. prog_inline_first. prog_skip. Qed.
imports: FCF.FCF