fact: Fixpoint all_fins (n : nat) : list (Fin.t n) := if n is S n' then Fin.F1 :: map Fin.FS (all_fins n') else nil.
imports: Undecidability.StackMachines(BSM BSM.bsm_defs) Undecidability.TM(SBTM Util.SBTM_facts) Undecidability.Shared.Libs.DLW(vec subcode sss) PeanoNat List Lia ssreflect ssrbool ssrfun