proposition: Lemma dec_red X (p : X -> Prop) Y (q : Y -> Prop) : p ⪯ q -> decidable q -> decidable p.
proof: Proof. unfold decidable, decider, reduces, reduction, reflects. intros [f] [d]. exists (fun x => d (f x)). firstorder easy. Qed.
imports: Undecidability.Synthetic.Definitions