proposition: Lemma semi_decidable_red (X Y : Type) (p : X -> Prop) (q : Y -> Prop) : p ⪯ q -> semi_decidable q -> semi_decidable p.
proof: Proof. intros [f Hf] [g Hg]. exists (fun x n => g (f x) n). firstorder. Qed.
imports: Undecidability.Synthetic(ReducibilityFacts DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts MoreEnumerabilityFacts) List Undecidability.Shared(Dec)