proposition: Lemma dec_ldec (P:term -> Prop) (f: term -> bool) {If : computable f}: (forall x, reflect (P x) (f x)) ->ldec P.
proof: Proof. intros H. exists (ext f). split. Lproc. intros s. eexists. split. - Lsimpl. reflexivity. - destruct (H s);assumption. Qed.