proposition: Lemma step_nop_transition (c : mconfig sig (state M1) n) : haltConf c = true -> step (lift_confL c) = lift_confR (initc (Mf (p1 (cstate c))) (ctapes c)).
proof: Proof. intros Halt. unfold lift_confL, lift_confR. cbn. unfold haltConf in Halt. unfold step at 1; cbn. rewrite Halt. f_equal. apply doAct_nop. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts