proposition: Lemma decidable_semi_decidable {X} {p : X -> Prop} : decidable p -> semi_decidable p.
proof: Proof. intros [f H]. exists (fun x n => f x). intros x. unfold decider, reflects in H. rewrite H. firstorder. econstructor. Qed.
imports: Undecidability.Synthetic.DecidabilityFacts