proposition: Fact sss_compute_refl i P (st : mm_state) : (i, P) // st ->> st.
proof: Proof. exists 0. by apply: in_sss_steps_0. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun