fact: Fixpoint to_nat (r : t) : nat := match r with mk rs => to_nat' to_nat rs end.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia