proposition: Theorem MuRec_computable_to_L_computable {k} (R : Vector.t nat k -> nat -> Prop) : MuRec_computable R -> L_computable R.
proof: Proof. eapply HaltMuRec_to_HaltL.computable_MuRec_to_L. Qed.
imports: Undecidability.L(L HaltMuRec_to_HaltL) Undecidability.MuRec(MuRec)