proposition: Theorem in_oc_supp_complete : forall (A B C : Set){eqdc : EqDec C}(c : OracleComp A B C) x (S : Set)(eqds : EqDec S)(o : S -> A -> Comp (B * S))(s : S) s', In (x, s') (getSupport (c _ _ o s)) -> in_oc_supp x c .
proof: Proof. induction c; intuition; repeat simp_in_support. econstructor. Local Opaque getSupport. simpl in *. repeat simp_in_support. destruct x. simpl. destruct p. simpl. econstructor. eapply (@IHc _ _ (S * S0)%type). eapply H1. simpl in *. repeat simp_in_support. econstructor. intuition. assert (EqDec C). eapply oc_EqDec. eapply c. intuition. assert (B * S). eapply comp_base_exists. eapply o0. trivial. intuition. intuition. intuition. assert (EqDec (B * S)). eapply comp_EqDec. eapply o0; trivial. eapply EqDec_pair_l. eapply H2. trivial. simpl in *. repeat simp_in_support. destruct x0. econstructor. eapply (@H0 _ S). eapply H2. eapply (@H _ _ _ S). eapply H3. Grab Existential Variables. eapply EqDec_pair_l. eauto. trivial. Qed.
imports: FCF PRF RndInList