proposition: Theorem compFold_oc_equiv : forall (A B S : Set)(eqdb : EqDec B)(eqds : EqDec S)(O : S -> A -> Comp (B * S))(lsa : list A)(initS : S), comp_spec eq (compFold _ (fun (acc : list B * S) (d : A) => [rs, s]<-2 acc; z <-$ O s d; [r, s0]<-2 z; ret (rs ++ r :: nil, s0)) (nil, initS) lsa) ((oc_compMap _ (fun a : A => query a) lsa) S _ O initS).
proof: Proof. intuition. eapply comp_spec_eq_trans. eapply compFold_oc_equiv_h. fcf_ident_expand_r. fcf_skip. simpl. fcf_spec_ret. Qed.
imports: FCF.FCF FCF.CompFold FCF.PRF