proposition: Theorem comp_fold_ext : forall (A B: Set)(eqd : EqDec A)(c1 c2 : A -> B -> Comp A)(ls : list B)(init : A), (forall a b, comp_spec eq (c1 a b) (c2 a b)) -> comp_spec eq (compFold _ c1 init ls) (compFold _ c2 init ls).
proof: Proof. intuition. eapply compFold_eq. eapply list_pred_eq. intuition. subst. eauto. Qed.
imports: FCF.FCF