fact: Fixpoint decode {X : Type} (L : list X) (i : Fin.t (length L)) : X := (match L return Fin.t (length L) -> X with | [] => fun j => Fin.case0 (fun=> X) j | x :: L' => fun j => Fin.caseS' j (fun=> X) x (fun j' => decode L' j') end) i.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun