proposition: Lemma case_None (o : option bool) {X} (c2 : X) c1 : (if! o is Some w then c1 w else c2 = c2 /\ o = None) \/ (exists w, (if! o is Some w then c1 w else c2) = c1 w /\ o = Some w).
proof: Proof. destruct o as [ [] | ]. right. eauto. right. eauto. eauto. 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)