proposition: Fact pctm_progress_BR P i j p t st : (i,[BR j p]) <sc P -> P // (if rd t then j else p,t) ->> st -> P // (i,t) -+> st.
proof: Proof. solve progress. Qed.
imports: List Bool Arith Lia Undecidability.Shared.Libs.DLW(subcode sss) Undecidability.TM(SBTM)