proposition: Lemma decides_false_rw: forall f P, Decides f P -> forall i, Run (f i) false <-> ~ P i.
proof: Proof. split; intros. { eauto using decides_run_false_to_not_in. } eauto using decides_not_in_to_run_false. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop