proposition: Lemma L_computable_can_closed k R: L_computable_closed R <-> L_computable (k:=k) R.
proof: Proof. split. - intros (s & _ & H). exists s. exact H. - intros (s & H). unshelve edestruct (@total_decodable_closed_new nat _ _ k s) as (s' & Hcl & Hs'). + intros v o. rewrite <- eval_iff. intros. eapply (H v). unfold apply_to in H0. revert H0. now rewrite many_app_eq_nat. + unfold apply_to in Hs'. exists s'. split. change (closed s'). Lproc. intros v. split. * intros m. specialize (H v) as [H1 H2]. rewrite H1. rewrite !eval_iff. rewrite <- !many_app_eq_nat. now rewrite Hs'. * intros o. rewrite eval_iff. rewrite <- many_app_eq_nat. rewrite Hs'. rewrite <- eval_iff. rewrite many_app_eq_nat. eapply H. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)