proposition: Lemma decides_or : forall p P, Decides p P -> forall i, P i \/ ~ P i.
proof: Proof. intros. destruct decides_to_run with (i:= i) (p:= p) (L:= P) as ([], Ha); auto. - left. apply decides_run_true_to_in with (p:= p); auto. - right. apply decides_run_false_to_not_in with (p:= p); auto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop