proposition: Lemma case_Some_true o {X} (c1 c2 : X) : (if! o is Some true then c1 else c2 = c1 /\ o = Some true) \/ (if! o is Some true then c1 else c2 = c2 /\ o <> Some true).
proof: Proof. Proof using M. destruct o as [ [] | ]; firstorder congruence. Qed.
imports: Undecidability.TM.KOSBTM.KOSBTM Undecidability.Shared.Libs.PSL.Vectors.FinNotation Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Shared.Libs.PSL.EqDec List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(bsm_defs)