proposition: Theorem compFold_oc_equiv_h : forall (A B S : Set)(eqdb : EqDec B)(eqds : EqDec S)(O : S -> A -> Comp (B * S))(lsa : list A)(initS : S)(lsb : list B), 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)) (lsb, initS) lsa) ([lsb', s'] <-$2 ((oc_compMap _ (fun a : A => query a) lsa) S _ O initS); ret (lsb ++ lsb', s')).
proof: Proof. induction lsa; intuition; simpl. fcf_inline_first. fcf_simp. rewrite app_nil_r. fcf_spec_ret. fcf_inline_first. fcf_skip. eapply comp_spec_eq_trans. eapply IHlsa. fcf_inline_first. fcf_skip. fcf_inline_first. fcf_simp. rewrite <- app_assoc. simpl. fcf_spec_ret. Qed.
imports: FCF.FCF FCF.CompFold FCF.PRF