fact: Definition encode_sig {X : Type} (HX : forall (x y : X), {x = y} + {x <> y}) {L : list X} (HL : forall x, In x L) (x : X) : {i : Fin.t (length L) | decode L i = x }.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun