proposition: Theorem oc_comp_wf : forall (A B C : Set)(c : OracleComp A B C), well_formed_oc c -> forall (S : Set)(eqds : EqDec S)(o : S -> A -> Comp (B * S))(s : S), (forall a b, well_formed_comp (o a b)) -> well_formed_comp (c _ _ o s).
proof: Proof. induction 1; intuition; simpl in *; intuition. eapply well_formed_Bind; intuition. eapply IHwell_formed_oc; intuition. eapply well_formed_Bind; intuition. eapply well_formed_Ret. eapply well_formed_Ret. eapply well_formed_Bind; intuition. eapply well_formed_Ret. eapply well_formed_Bind; intuition. destruct b. eauto. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms