proposition: Lemma step_comp_liftR f (c : mconfig sig (state (Mf f)) n) : step (lift_confR c) = lift_confR (step c).
proof: Proof. destruct c. unfold lift_confR, step. cbn. destruct (trans _) eqn:E. cbn. reflexivity. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts