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