proposition: Lemma decides_run_true_to_in: forall p L i, Decides p L -> Run (p i) true -> L i.
proof: Proof. intros. apply decides_to_recognizes in H. apply recognizes_run_true_to_in with (p:=p); auto. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop