proposition: Lemma code_of : forall f : input -> prog, exists m, CodeOf f m.
proof: Proof. intros. destruct (closure_of (fun x => f)) as (c, hc). exists (c input_inhabited). unfold CodeOf. unfold ClosureOf in *. intros. rewrite hc. reflexivity. Qed.
imports: Coq.Setoids.Setoid Coq.Bool.Bool Coq.Logic.Classical_Prop