wilbowma

{-# OPTIONS --guarded #-}


open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans)
open import Data.Unit using (⊤; tt)
open import Data.Nat -- using (ℕ; _+_; suc; _<_)
open import Data.Nat.Properties
open import Data.Fin using (Fin; fromℕ; fromℕ<)
open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map)