fact: Definition InT {X} (x:X) := fix InT {n} (v : t X n) := match v with | nil _ => (False : Type) | cons _ y _ v => ((x=y) + InT v)%type end.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors)