proposition: Theorem oc_compMap_qam : forall (A B C D : Set)(eqdb : EqDec B)(c : A -> OracleComp C D B ) (ls : list A)(q : nat), (forall a, queries_at_most (c a) q) -> queries_at_most (oc_compMap _ c ls) (length ls * q)%nat.
proof: Proof. induction ls; intuition; simpl in *. econstructor. econstructor. auto. intuition. econstructor. econstructor. auto. intuition. econstructor. lia. Qed.
imports: FCF.FCF FCF.CompFold FCF.PRF