proposition: Theorem oc_comp_invariant_f : forall (A B C : Set)(c : OracleComp A B C)(S : Set)(f : S -> bool) (eqds : EqDec S) (o : S -> A -> Comp (B * S))(s : S), (forall a b c d, In (a, b) (getSupport (o c d)) -> f c = true -> f b = true) -> f s = true -> forall a b, In (a, b) (getSupport (c _ _ o s)) -> f b = true.
proof: Proof. intuition. eapply (@oc_comp_invariant _ _ _ _ _ (fun x => f x = true)); intuition. eapply H. eapply H2. eapply H3. eapply H0. eapply H1. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms