proposition: Lemma Halt_BSM_iff P : Halt_BSM P <-> BSM_HALTING P.
proof: Proof. destruct P as (n & i & P & v); cbn. split. - intros (c' & v' & H % eval_iff). eexists. eauto. - intros [(c', v') H % eval_iff]. eauto. Qed.
imports: Undecidability.StackMachines.BSM List Bool Lia Nat Undecidability.Shared.Libs.DLW(list_bool pos vec sss)