proposition: Fact ra_compiler_cst c : ra_compiler_stm (ra_cst c).
proof: Proof. red; simpl; intros i p o m H1 H2 H3. exists (mm_set o m c i); intros v e H4 _; split. 2: exists c; cbv; auto. revert H4; vec nil v; clear v. intros H4 x E; simpl in E; subst x. rewrite mm_set_length. destruct mm_set_progress with (dst := o) (zero := m) (n := c) (i := i) (e := e) as (e' & G1 & G2); auto; try lia. exists e'; split; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils finite pos vec subcode sss) Undecidability.MinskyMachines(env mme_defs mme_utils) Undecidability.MuRec.Util(recalg)