proposition: Theorem compFold_cons : forall (A B : Set)(eqda : EqDec A)(c : A -> B -> Comp A)(ls : list B) b (a : A), comp_spec eq (compFold _ c a (b :: ls)) (a' <-$ c a b; compFold _ c a' ls).
proof: Proof. intuition. simpl. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF Permutation