proposition: Lemma closure_of_negative_rw {p} {f}: ClosureOf f p -> forall i j, Negative (Call (p j) i) <-> Negative (f j i).
proof: Proof. intros. repeat rewrite negative_rw. rewrite (closure_of_run_rw H). reflexivity. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop