proposition: Lemma decidable_to_recognizable: forall L, Decidable L -> Recognizable L.
proof: Proof. intros. destruct H as (p, H). destruct H. apply recognizable_def with (p:=p). assumption. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop