proposition: Lemma decides_true_rw {f} {P}: Decides f P -> forall i, Run (f i) true <-> P i.
proof: Proof. split; intros. { eapply decides_run_true_to_in; eauto. } eauto using decides_in_to_run_true. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop