proposition: Theorem ExpROM_swap_spec : forall (D1 R1 : Set) (A1 : Set) (c1 : OracleComp D1 R1 A1) (D2 R2 : Set) (A2 : Set) (c2 : OracleComp D2 R2 A2) (eqdr1 : EqDec R1)(eqdr2 : EqDec R2) (eqda1 : EqDec A1)(eqda2 : EqDec A2) (S : Set)(eqds : EqDec S) (o1 : S -> D1 -> Comp (R1 * S)) (o2 : S -> D2 -> Comp (R2 * S)) s, (forall s d1 d2, comp_spec eq ([x2, s2] <-$2 o1 s d1; [x3, s3] <-$2 o2 s2 d2; ret ((x2, x3), s3)) ([x3, s2] <-$2 o2 s d2; [x2, s3] <-$2 o1 s2 d1; ret ((x2, x3), s3)) ) -> comp_spec eq ([x2, s2] <-$2 c1 _ _ o1 s; [x3, s3] <-$2 c2 _ _ o2 s2; ret ((x2, x3), s3)) ([x3, s2] <-$2 c2 _ _ o2 s; [x2, s3] <-$2 c1 _ _ o1 s2; ret ((x2, x3), s3)).
proof: Proof. intuition idtac. eapply ExpROM_swap_spec_h. intuition idtac. intuition idtac. eapply ExpROM_query_swap_spec; intuition idtac. eauto. Qed.
imports: FCF FCF.PRF Permutation