proposition: Theorem reducible_decidable: forall A B, A <=m B -> Decidable B -> Decidable A.
proof: Proof. intros A B (f, Hred) (M, (Hr, Hd)). destruct (code_of M) as (R, HR). apply decidable_def with (p:=fun w => Call R (f w)). split. - apply recognizes_def. intros. rewrite (code_of_run_rw HR). rewrite (recognizes_rw Hr). rewrite (reduction_rw Hred). reflexivity. - apply decider_def. intros. rewrite (code_of_halt_rw HR). auto using decider_to_halt. Qed.
imports: Coq.Setoids.Setoid Turing.Turing