proposition: Lemma step_comp_liftL (c : mconfig sig (state M1) n) : haltConf c = false -> step (lift_confL c) = lift_confL (step c).
proof: Proof. unfold lift_confL, step, haltConf. cbn. destruct c as [q t]; cbn in *. intros H. rewrite H. destruct (trans _) eqn:E. cbn. reflexivity. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts