proposition: Theorem compMap_map_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 : B -> D)(f4 : C -> D), (forall a, comp_spec (fun b c => f3 b = f4 c) (f1 a) (f2 a)) -> comp_spec eq (lsb <-$ compMap _ f1 ls; ret (map f3 lsb)) (compMap _ (fun a => b <-$ f2 a; ret (f4 b)) ls).
proof: Proof. intuition. eapply compMap_fission_eq; intuition. simpl. eapply comp_spec_eq_refl. simpl. prog_simp. eapply comp_spec_ret. congruence. Qed.
imports: FCF.FCF