proposition: Lemma code_of_halt_rw {p} {f}: CodeOf f p -> forall i, Halt (Call p i) <-> Halt (f i).
proof: Proof. intros. repeat rewrite halt_rw. split; intros (x, Hx); exists x. - rewrite (code_of_run_rw H) in Hx. assumption. - rewrite (code_of_run_rw H). assumption. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop