Factor some code out into Utils

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Utils.agda

@@ -1,8 +1,10 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
-open import Data.Product as Prod using (_×_)
+open import Data.Product as Prod using (Σ; _×_; _,_; proj₁; proj₂)
 open import Data.Nat using (ℕ; suc)
+open import Data.Fin as Fin using (Fin; suc; zero)
+open import Data.Fin.Properties using (suc-injective)
 open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
@@ -106,3 +108,24 @@ _∧_ P Q a = P a × Q a
 
 it : ∀ {a} {A : Set a} {{_ : A}} → A
 it {{x}} = x
+
+z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (Fin.zero ≡ Fin.suc f)
+z≢sf f ()
+
+z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
+z≢mapsfs [] = []
+z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+fins : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+fins 0 = ([] , empty)
+fins (suc n') =
+    let
+        (inds' , unids') = fins n'
+    in
+        ( zero ∷ mapˡ suc inds'
+        , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+        )
+
+fins-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ (proj₁ (fins n))
+fins-complete (suc n') zero = here refl
+fins-complete (suc n') (suc f') = there (x∈xs⇒fx∈fxs suc (fins-complete n' f'))