proposition: Lemma recognizes_def_2: forall p (L:lang), (forall i, Run (p i) true -> L i) -> (forall i, L i -> Run (p i) true) -> Recognizes p L.
proof: Proof. intros. unfold Recognizes. intros; split; auto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop