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