proposition: Lemma code_of_run_rw {p} {f}: CodeOf f p -> forall i b, Run (Call p i) b <-> Run (f i) b.
proof: Proof. unfold CodeOf. intuition. - inversion_clear H0. apply H. assumption. - constructor. apply H. assumption. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop