proposition: Lemma sss_compute_progress P st st' : P // st ->> st' -> st <> st' -> P // st -+> st'.
proof: Proof. move=> [[|k]]. - by move=> /sss_steps_0_inv. - move=> Hk _. exists (S k). by split; [lia|]. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun