proposition: Theorem compFold_ret_eq : forall (A: Type)(B : Set)(eqdb : EqDec B)(ls : list A)(f : B -> A -> B) init, comp_spec eq (compFold _ (fun b a => ret (f b a)) init ls) (ret (fold_left f ls init)).
proof: Proof. induction ls; intuition; simpl in *. eapply comp_spec_eq_refl. comp_simp. eauto. Qed.
imports: FCF.FCF Permutation