proposition: Theorem compMap_oc_spec : forall (C D : Set)(P2 : C -> D -> Prop)(A B : Set)(P1 : A -> B -> Prop)(eqdc : EqDec C)(eqdd : EqDec D)(E F S: Set)(eqds : EqDec S)(ls1 : list A)(ls2 : list B)(c1 : A -> Comp C)(c2 : B -> OracleComp E F D)o (s : S), list_pred P1 ls1 ls2 -> (forall a b z, P1 a b -> comp_spec (fun x y => P2 x (fst y)) (c1 a) (c2 b _ _ o z)) -> comp_spec (fun a b => list_pred P2 a (fst b)) (compMap _ c1 ls1) ((oc_compMap _ c2 ls2) _ _ o s).
proof: Proof. induction ls1; inversion 1; subst; intuition; simpl in *. comp_simp. eapply comp_spec_ret; simpl; econstructor. simpl. comp_skip. comp_simp. comp_skip. comp_simp. eapply comp_spec_ret; intuition. simpl. econstructor; eauto. Qed.
imports: FCF.FCF FCF.CompFold