proposition: Lemma recognizes_impl: forall p L1 L2, Equiv L1 L2 -> Recognizes p L1 -> Recognizes p L2.
proof: Proof. intros. unfold Recognizes in *. intros. rewrite H0. apply H. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop