proposition: Lemma decidable_complement_semi_decidable {X} {p : X -> Prop} : decidable p -> semi_decidable (complement p).
proof: Proof. intros H. now eapply decidable_semi_decidable, dec_compl. Qed.
imports: Undecidability.Synthetic.DecidabilityFacts