fact: Fixpoint all_fins (n : nat) : list (Fin.t n) := match n with | 0 => nil | S n => Fin.F1 :: map Fin.FS (all_fins n) end.
imports: Undecidability.Shared.Libs.PSL(BasicDefinitions) Undecidability.Shared.Libs.PSL(FiniteTypes.FinTypes) Undecidability.Shared.Libs.PSL(Vectors.Vectors)