proposition: Theorem ExpROM_seq_eq : forall (A B : Set) (eqdb : EqDec B) (c1a c1b : OracleComp DomainRO RangeRO A) (c2a c2b : A -> OracleComp DomainRO RangeRO B) v s, (forall x, evalDist (c1a _ _ (randomFunc rndRange DomainRO_EqDec) s) x == evalDist (c1b _ _ (randomFunc rndRange DomainRO_EqDec) s) x) -> (forall x1 s v, evalDist (z <-$ (c2a x1) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (randomFunc rndRange DomainRO_EqDec) s; [a, _]<-2 z; ret a) v == evalDist (z <-$ (c2b x1) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (randomFunc rndRange DomainRO_EqDec) s; [a, _]<-2 z; ret a) v ) -> evalDist (z <-$ (x1 <--$ c1a; c2a x1) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (randomFunc rndRange DomainRO_EqDec) s; [a, _]<-2 z; ret a) v == evalDist (z <-$ (x1 <--$ c1b; c2b x1) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (randomFunc rndRange DomainRO_EqDec) s; [a, _]<-2 z; ret a) v.
proof: Proof. intuition idtac. Local Opaque evalDist. simpl. fcf_inline_first. fcf_skip. fcf_simp. eauto. Local Transparent evalDist. Qed.
imports: FCF FCF.PRF Permutation