proposition: Lemma case_pos2 (v : pos 2) : (v = Fin.F1) + (v = Fin.FS Fin.F1).
proof: Proof. have [?|] := pos_S_inv v; first by left. move=> [w] ->. right. have [->|] := pos_S_inv w; first done. move=> [?]. exfalso. by apply: pos_O_inv. Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun