proposition: Theorem comp_spec_event_equiv : forall (A B : Set){eqda : EqDec A}{eqdb : EqDec B}(c1 : Comp A)(c2 : Comp B)(f1 : A -> bool)(f2 : B -> bool)(P : bool -> bool -> Prop), comp_spec (fun a b => P (f1 a) (f2 b)) c1 c2 -> comp_spec P (x <-$ c1; ret (f1 x)) (x <-$ c2; ret (f2 x)).
proof: Proof. intuition. eapply comp_spec_seq. apply true. apply true. eauto. intuition. eapply comp_spec_ret. trivial. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1