proposition: Theorem oc_comp_spec_eq : forall (A B C : Set)(c : OracleComp A B C), forall (eqdb : EqDec B) (eqdc : EqDec C)(S1 S2 : Set)(o1 : S1 -> A -> Comp (B * S1))(o2 : S2 -> A -> Comp (B * S2)) eqds1 eqds2 s1 s2 (P : S1 -> S2 -> Prop), P s1 s2 -> (forall a x1 x2, P x1 x2 -> comp_spec (fun y1 y2 => fst y1 = fst y2 /\ P (snd y1) (snd y2)) (o1 x1 a) (o2 x2 a)) -> comp_spec (fun a b => fst a = fst b /\ P (snd a) (snd b)) (c _ eqds1 o1 s1) (c _ eqds2 o2 s2).
proof: Proof. induction c; intuition; simpl in *. eapply (@comp_spec_consequence _ _ (@pair_EqDec B S1 eqdb eqds1) _ (@pair_EqDec B S2 eqdb eqds2)). eapply H0; intuition. intuition. assert (EqDec C). eapply EqDec_pair_l; eauto. eapply (@comp_spec_seq _ _ (fun a b => fst a = fst b /\ fst (snd a) = fst (snd b) /\ P (snd (snd a)) (snd (snd b)) )) ; eauto. intuition. eapply oc_base_exists; eauto; intuition. assert (B * S). eapply oc_base_exists. eauto. intuition. assert (B' * S1). eapply comp_base_exists. eauto. intuition. intuition. intuition. eapply oc_base_exists; eauto; intuition. assert (B * S). eapply oc_base_exists. eauto. intuition. assert (B' * S1). eapply comp_base_exists. eauto. intuition. intuition. eapply comp_spec_consequence. eapply (IHc _ _ _ _ _ _ _ _ _ _ (fun p1 p2 => fst p1 = fst p2 /\ P (snd p1) (snd p2))). simpl; intuition. intuition. simpl in *. subst. eapply comp_spec_seq. intuition. assert (B * S). eapply oc_base_exists. eauto. intuition. assert (B' * S1). eapply comp_base_exists. eapply o1; intuition. intuition. intuition. intuition. assert (B * S). eapply oc_base_exists. eauto. intuition. assert (B' * S1). eapply comp_base_exists. eapply o1; intuition. intuition. intuition. eapply H. eauto. intuition. intuition. eapply comp_spec_ret. simpl in *; intuition. destruct b2; simpl in *. destruct p; simpl in *; intuition. inversion H7; clear H7; subst. intuition. destruct b2; simpl in *. subst. simpl. intuition. intuition. intuition. simpl in *. subst. eapply comp_spec_ret. simpl in *. destruct b; simpl in *. intuition. eapply comp_spec_seq_eq; intuition. eapply comp_base_exists; intuition. eapply comp_base_exists; intuition. eapply comp_spec_eq_refl. eapply comp_spec_ret; simpl; intuition. assert (EqDec C). eapply oc_EqDec. eapply c. intuition. intuition. assert (B * S1). eapply comp_base_exists. eauto. intuition. intuition. eapply comp_spec_seq. intuition. eapply oc_base_exists. eapply o. eapply oc_base_exists. eauto. intuition. assert (B * S1). eapply comp_base_exists. eapply o1. intuition. trivial. intuition. intuition. assert (B * S1). eapply comp_base_exists. eapply o1; intuition. intuition. intuition. eapply oc_base_exists. eapply o. eapply oc_base_exists. eauto. intuition. assert (B * S1). eapply comp_base_exists. eapply o1. intuition. trivial. intuition. intuition. assert (B * S1). eapply comp_base_exists. eapply o1; intuition. intuition. eapply IHc. eauto. intuition. intuition. simpl in *. subst. destruct b0. simpl. eapply H; intuition. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1