proposition: Theorem oc_compMap_eq : forall (A B C D : Set){eqd : EqDec D}(f1 f2 : A -> OracleComp B C D)(ls : list A) (S : Set){eqds : EqDec S} o (s : S), (forall s a, comp_spec eq ((f1 a) _ _ o s) ((f2 a) _ _ o s)) -> comp_spec eq ((oc_compMap _ f1 ls) _ _ o s) ((oc_compMap _ f2 ls) _ _ o s).
proof: Proof. induction ls; intuition; simpl in *. comp_simp. eapply comp_spec_eq_refl. comp_skip. comp_skip. comp_simp. eapply comp_spec_eq_refl. Qed.
imports: FCF.FCF FCF.CompFold