proposition: Lemma compFold_spec : forall (A : Type)(C D : Set)(P2 : list A -> C -> D -> Prop)(eqdc : EqDec C)(eqdd : EqDec D)(lsa : list A)(c1 : C -> A -> Comp C)(c2 : D -> A -> Comp D) init1 init2, P2 lsa init1 init2 -> (forall a lsa c d, P2 (a :: lsa) c d -> comp_spec (P2 lsa) (c1 c a) (c2 d a)) -> comp_spec (P2 nil) (compFold _ c1 init1 lsa) (compFold _ c2 init2 lsa).
proof: Proof. induction lsa; intuition; simpl. eapply comp_spec_ret; intuition. eapply comp_spec_seq; intuition. eapply H0; eauto. intuition. Qed.
imports: FCF.FCF