proposition: Lemma compFold_wf : forall (A : Set)(B : Type)(eqd : EqDec A)(c : A -> B -> Comp A)(ls : list B) init, (forall a b, well_formed_comp (c a b)) -> well_formed_comp (compFold _ c init ls).
proof: Proof. induction ls; intuition. unfold compFold. wftac. unfold compFold. fold compFold. wftac. Qed.
imports: FCF.FCF