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