Generic.ReflectionTerm

module Generic.ReflectionTerm where

open import Generic.Core
open import Generic.Certified

import Agda.Builtin.Reflection as R

data TermAtomCode : Type₀ where
  natAtom nameAtom metaAtom literalAtom stringAtom : TermAtomCode

TermAtom : TermAtomCode → Type₀
TermAtom natAtom = ℕ
TermAtom nameAtom = R.Name
TermAtom metaAtom = R.Meta
TermAtom literalAtom = R.Literal
TermAtom stringAtom = String

TermAtoms : AtomUniverse ℓ-zero
TermAtoms = atomUniverse TermAtomCode TermAtom

termI sortI patternI clauseI listArgTermI argTermI absTermI listClauseI
  listArgPatternI argPatternI telescopeI telEntryI argInfoI modalityI
  visibilityI relevanceI quantityI : Fin 17
termI = Fin.zero
sortI = Fin.suc Fin.zero
patternI = Fin.suc (Fin.suc Fin.zero)
clauseI = Fin.suc (Fin.suc (Fin.suc Fin.zero))
listArgTermI = Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))
argTermI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))
absTermI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))
listClauseI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))
listArgPatternI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))
argPatternI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))
telescopeI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))
telEntryI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))
argInfoI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))
modalityI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))
visibilityI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))
relevanceI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))))
quantityI = Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))))

TermDesc : Fin 17 → TyDesc TermAtoms 17
TermDesc Fin.zero =
  dataD
    ( κ₂ (α natAtom) (μ listArgTermI)
    ∷ κ₂ (α nameAtom) (μ listArgTermI)
    ∷ κ₂ (α nameAtom) (μ listArgTermI)
    ∷ κ₂ (μ visibilityI) (μ absTermI)
    ∷ κ₂ (μ listClauseI) (μ listArgTermI)
    ∷ κ₂ (μ argTermI) (μ absTermI)
    ∷ κ₁ (μ sortI)
    ∷ κ₁ (α literalAtom)
    ∷ κ₂ (α metaAtom) (μ listArgTermI)
    ∷ κ₀
    ∷ [])
TermDesc (Fin.suc Fin.zero) =
  dataD
    ( κ₁ (μ termI)
    ∷ κ₁ (α natAtom)
    ∷ κ₁ (μ termI)
    ∷ κ₁ (α natAtom)
    ∷ κ₁ (α natAtom)
    ∷ κ₀
    ∷ [])
TermDesc (Fin.suc (Fin.suc Fin.zero)) =
  dataD
    ( κ₂ (α nameAtom) (μ listArgPatternI)
    ∷ κ₁ (μ termI)
    ∷ κ₁ (α natAtom)
    ∷ κ₁ (α literalAtom)
    ∷ κ₁ (α nameAtom)
    ∷ κ₁ (α natAtom)
    ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc Fin.zero))) =
  dataD
    ( κ₃ (μ telescopeI) (μ listArgPatternI) (μ termI)
    ∷ κ₂ (μ telescopeI) (μ listArgPatternI)
    ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))) =
  dataD (κ₀ ∷ κ₂ (μ argTermI) (μ listArgTermI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))) =
  dataD (κ₂ (μ argInfoI) (μ termI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))) =
  dataD (κ₂ (α stringAtom) (μ termI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))) =
  dataD (κ₀ ∷ κ₂ (μ clauseI) (μ listClauseI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))) =
  dataD (κ₀ ∷ κ₂ (μ argPatternI) (μ listArgPatternI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))) =
  dataD (κ₂ (μ argInfoI) (μ patternI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))) =
  dataD (κ₀ ∷ κ₂ (μ telEntryI) (μ telescopeI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))) =
  dataD (κ₂ (α stringAtom) (μ argTermI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))) =
  dataD (κ₂ (μ visibilityI) (μ modalityI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))) =
  dataD (κ₂ (μ relevanceI) (μ quantityI) ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))) =
  dataD (κ₀ ∷ κ₀ ∷ κ₀ ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))))) =
  dataD (κ₀ ∷ κ₀ ∷ [])
TermDesc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))))) =
  dataD (κ₀ ∷ κ₀ ∷ [])

TermCode : Type₀
TermCode = CodeIx TermAtoms TermDesc (TermDesc termI)

mutual
  encodeTerm : R.Term → CodeIx TermAtoms TermDesc (TermDesc termI)
  encodeTerm (R.var x args) = ν₂ ι₀ (atomIx x) (recIx (encodeListArgTerm args))
  encodeTerm (R.con c args) = ν₂ ι₁ (atomIx c) (recIx (encodeListArgTerm args))
  encodeTerm (R.def f args) = ν₂ ι₂ (atomIx f) (recIx (encodeListArgTerm args))
  encodeTerm (R.lam v t) = ν₂ ι₃ (recIx (encodeVisibility v)) (recIx (encodeAbsTerm t))
  encodeTerm (R.pat-lam cs args) = ν₂ ι₄ (recIx (encodeListClause cs)) (recIx (encodeListArgTerm args))
  encodeTerm (R.pi a b) = ν₂ ι₅ (recIx (encodeArgTerm a)) (recIx (encodeAbsTerm b))
  encodeTerm (R.agda-sort s) = ν₁ ι₆ (recIx (encodeSort s))
  encodeTerm (R.lit l) = ν₁ ι₇ (atomIx l)
  encodeTerm (R.meta x args) = ν₂ ι₈ (atomIx x) (recIx (encodeListArgTerm args))
  encodeTerm R.unknown = ν₀ ι₉

  encodeSort : R.Sort → CodeIx TermAtoms TermDesc (TermDesc sortI)
  encodeSort (R.set t) = ν₁ ι₀ (recIx (encodeTerm t))
  encodeSort (R.lit n) = ν₁ ι₁ (atomIx n)
  encodeSort (R.prop t) = ν₁ ι₂ (recIx (encodeTerm t))
  encodeSort (R.propLit n) = ν₁ ι₃ (atomIx n)
  encodeSort (R.inf n) = ν₁ ι₄ (atomIx n)
  encodeSort R.unknown = ν₀ ι₅

  encodePattern : R.Pattern → CodeIx TermAtoms TermDesc (TermDesc patternI)
  encodePattern (R.con c ps) = ν₂ ι₀ (atomIx c) (recIx (encodeListArgPattern ps))
  encodePattern (R.dot t) = ν₁ ι₁ (recIx (encodeTerm t))
  encodePattern (R.var x) = ν₁ ι₂ (atomIx x)
  encodePattern (R.lit l) = ν₁ ι₃ (atomIx l)
  encodePattern (R.proj f) = ν₁ ι₄ (atomIx f)
  encodePattern (R.absurd x) = ν₁ ι₅ (atomIx x)

  encodeClause : R.Clause → CodeIx TermAtoms TermDesc (TermDesc clauseI)
  encodeClause (R.clause tel ps t) = ν₃ ι₀ (recIx (encodeTelescope tel)) (recIx (encodeListArgPattern ps)) (recIx (encodeTerm t))
  encodeClause (R.absurd-clause tel ps) = ν₂ ι₁ (recIx (encodeTelescope tel)) (recIx (encodeListArgPattern ps))

  encodeListArgTerm : List (R.Arg R.Term) → CodeIx TermAtoms TermDesc (TermDesc listArgTermI)
  encodeListArgTerm [] = ν₀ ι₀
  encodeListArgTerm (x ∷ xs) = ν₂ ι₁ (recIx (encodeArgTerm x)) (recIx (encodeListArgTerm xs))

  encodeArgTerm : R.Arg R.Term → CodeIx TermAtoms TermDesc (TermDesc argTermI)
  encodeArgTerm (R.arg i x) = ν₂ ι₀ (recIx (encodeArgInfo i)) (recIx (encodeTerm x))

  encodeAbsTerm : R.Abs R.Term → CodeIx TermAtoms TermDesc (TermDesc absTermI)
  encodeAbsTerm (R.abs s x) = ν₂ ι₀ (atomIx s) (recIx (encodeTerm x))

  encodeListClause : List R.Clause → CodeIx TermAtoms TermDesc (TermDesc listClauseI)
  encodeListClause [] = ν₀ ι₀
  encodeListClause (x ∷ xs) = ν₂ ι₁ (recIx (encodeClause x)) (recIx (encodeListClause xs))

  encodeListArgPattern : List (R.Arg R.Pattern) → CodeIx TermAtoms TermDesc (TermDesc listArgPatternI)
  encodeListArgPattern [] = ν₀ ι₀
  encodeListArgPattern (x ∷ xs) = ν₂ ι₁ (recIx (encodeArgPattern x)) (recIx (encodeListArgPattern xs))

  encodeArgPattern : R.Arg R.Pattern → CodeIx TermAtoms TermDesc (TermDesc argPatternI)
  encodeArgPattern (R.arg i x) = ν₂ ι₀ (recIx (encodeArgInfo i)) (recIx (encodePattern x))

  encodeTelescope : R.Telescope → CodeIx TermAtoms TermDesc (TermDesc telescopeI)
  encodeTelescope [] = ν₀ ι₀
  encodeTelescope (x ∷ xs) = ν₂ ι₁ (recIx (encodeTelEntry x)) (recIx (encodeTelescope xs))

  encodeTelEntry : Σ String (λ _ → R.Arg R.Type) → CodeIx TermAtoms TermDesc (TermDesc telEntryI)
  encodeTelEntry (s , a) = ν₂ ι₀ (atomIx s) (recIx (encodeArgTerm a))

  encodeArgInfo : R.ArgInfo → CodeIx TermAtoms TermDesc (TermDesc argInfoI)
  encodeArgInfo (R.arg-info v m) = ν₂ ι₀ (recIx (encodeVisibility v)) (recIx (encodeModality m))

  encodeModality : R.Modality → CodeIx TermAtoms TermDesc (TermDesc modalityI)
  encodeModality (R.modality r q) = ν₂ ι₀ (recIx (encodeRelevance r)) (recIx (encodeQuantity q))

  encodeVisibility : R.Visibility → CodeIx TermAtoms TermDesc (TermDesc visibilityI)
  encodeVisibility R.visible = ν₀ ι₀
  encodeVisibility R.hidden = ν₀ ι₁
  encodeVisibility R.instance′ = ν₀ ι₂

  encodeRelevance : R.Relevance → CodeIx TermAtoms TermDesc (TermDesc relevanceI)
  encodeRelevance R.relevant = ν₀ ι₀
  encodeRelevance R.irrelevant = ν₀ ι₁

  encodeQuantity : R.Quantity → CodeIx TermAtoms TermDesc (TermDesc quantityI)
  encodeQuantity R.quantity-0 = ν₀ ι₀
  encodeQuantity R.quantity-ω = ν₀ ι₁

mutual
  decodeTerm : CodeIx TermAtoms TermDesc (TermDesc termI) → R.Term
  decodeTerm (ν₂ ι₀ (atomIx x) (recIx args)) = R.var x (decodeListArgTerm args)
  decodeTerm (ν₂ ι₁ (atomIx c) (recIx args)) = R.con c (decodeListArgTerm args)
  decodeTerm (ν₂ ι₂ (atomIx f) (recIx args)) = R.def f (decodeListArgTerm args)
  decodeTerm (ν₂ ι₃ (recIx v) (recIx t)) = R.lam (decodeVisibility v) (decodeAbsTerm t)
  decodeTerm (ν₂ ι₄ (recIx cs) (recIx args)) = R.pat-lam (decodeListClause cs) (decodeListArgTerm args)
  decodeTerm (ν₂ ι₅ (recIx a) (recIx b)) = R.pi (decodeArgTerm a) (decodeAbsTerm b)
  decodeTerm (ν₁ ι₆ (recIx s)) = R.agda-sort (decodeSort s)
  decodeTerm (ν₁ ι₇ (atomIx l)) = R.lit l
  decodeTerm (ν₂ ι₈ (atomIx x) (recIx args)) = R.meta x (decodeListArgTerm args)
  decodeTerm (ν₀ ι₉) = R.unknown

  decodeSort : CodeIx TermAtoms TermDesc (TermDesc sortI) → R.Sort
  decodeSort (ν₁ ι₀ (recIx t)) = R.set (decodeTerm t)
  decodeSort (ν₁ ι₁ (atomIx n)) = R.lit n
  decodeSort (ν₁ ι₂ (recIx t)) = R.prop (decodeTerm t)
  decodeSort (ν₁ ι₃ (atomIx n)) = R.propLit n
  decodeSort (ν₁ ι₄ (atomIx n)) = R.inf n
  decodeSort (ν₀ ι₅) = R.unknown

  decodePattern : CodeIx TermAtoms TermDesc (TermDesc patternI) → R.Pattern
  decodePattern (ν₂ ι₀ (atomIx c) (recIx ps)) = R.con c (decodeListArgPattern ps)
  decodePattern (ν₁ ι₁ (recIx t)) = R.dot (decodeTerm t)
  decodePattern (ν₁ ι₂ (atomIx x)) = R.var x
  decodePattern (ν₁ ι₃ (atomIx l)) = R.lit l
  decodePattern (ν₁ ι₄ (atomIx f)) = R.proj f
  decodePattern (ν₁ ι₅ (atomIx x)) = R.absurd x

  decodeClause : CodeIx TermAtoms TermDesc (TermDesc clauseI) → R.Clause
  decodeClause (ν₃ ι₀ (recIx tel) (recIx ps) (recIx t)) = R.clause (decodeTelescope tel) (decodeListArgPattern ps) (decodeTerm t)
  decodeClause (ν₂ ι₁ (recIx tel) (recIx ps)) = R.absurd-clause (decodeTelescope tel) (decodeListArgPattern ps)

  decodeListArgTerm : CodeIx TermAtoms TermDesc (TermDesc listArgTermI) → List (R.Arg R.Term)
  decodeListArgTerm (ν₀ ι₀) = []
  decodeListArgTerm (ν₂ ι₁ (recIx x) (recIx xs)) = decodeArgTerm x ∷ decodeListArgTerm xs

  decodeArgTerm : CodeIx TermAtoms TermDesc (TermDesc argTermI) → R.Arg R.Term
  decodeArgTerm (ν₂ ι₀ (recIx i) (recIx x)) = R.arg (decodeArgInfo i) (decodeTerm x)

  decodeAbsTerm : CodeIx TermAtoms TermDesc (TermDesc absTermI) → R.Abs R.Term
  decodeAbsTerm (ν₂ ι₀ (atomIx s) (recIx x)) = R.abs s (decodeTerm x)

  decodeListClause : CodeIx TermAtoms TermDesc (TermDesc listClauseI) → List R.Clause
  decodeListClause (ν₀ ι₀) = []
  decodeListClause (ν₂ ι₁ (recIx x) (recIx xs)) = decodeClause x ∷ decodeListClause xs

  decodeListArgPattern : CodeIx TermAtoms TermDesc (TermDesc listArgPatternI) → List (R.Arg R.Pattern)
  decodeListArgPattern (ν₀ ι₀) = []
  decodeListArgPattern (ν₂ ι₁ (recIx x) (recIx xs)) = decodeArgPattern x ∷ decodeListArgPattern xs

  decodeArgPattern : CodeIx TermAtoms TermDesc (TermDesc argPatternI) → R.Arg R.Pattern
  decodeArgPattern (ν₂ ι₀ (recIx i) (recIx x)) = R.arg (decodeArgInfo i) (decodePattern x)

  decodeTelescope : CodeIx TermAtoms TermDesc (TermDesc telescopeI) → R.Telescope
  decodeTelescope (ν₀ ι₀) = []
  decodeTelescope (ν₂ ι₁ (recIx x) (recIx xs)) = decodeTelEntry x ∷ decodeTelescope xs

  decodeTelEntry : CodeIx TermAtoms TermDesc (TermDesc telEntryI) → Σ String (λ _ → R.Arg R.Type)
  decodeTelEntry (ν₂ ι₀ (atomIx s) (recIx a)) = s , decodeArgTerm a

  decodeArgInfo : CodeIx TermAtoms TermDesc (TermDesc argInfoI) → R.ArgInfo
  decodeArgInfo (ν₂ ι₀ (recIx v) (recIx m)) = R.arg-info (decodeVisibility v) (decodeModality m)

  decodeModality : CodeIx TermAtoms TermDesc (TermDesc modalityI) → R.Modality
  decodeModality (ν₂ ι₀ (recIx r) (recIx q)) = R.modality (decodeRelevance r) (decodeQuantity q)

  decodeVisibility : CodeIx TermAtoms TermDesc (TermDesc visibilityI) → R.Visibility
  decodeVisibility (ν₀ ι₀) = R.visible
  decodeVisibility (ν₀ ι₁) = R.hidden
  decodeVisibility (ν₀ ι₂) = R.instance′

  decodeRelevance : CodeIx TermAtoms TermDesc (TermDesc relevanceI) → R.Relevance
  decodeRelevance (ν₀ ι₀) = R.relevant
  decodeRelevance (ν₀ ι₁) = R.irrelevant

  decodeQuantity : CodeIx TermAtoms TermDesc (TermDesc quantityI) → R.Quantity
  decodeQuantity (ν₀ ι₀) = R.quantity-0
  decodeQuantity (ν₀ ι₁) = R.quantity-ω

mutual
  decode-encodeTerm : (t : R.Term) → decodeTerm (encodeTerm t) ≡ t
  decode-encodeTerm (R.var x args) i = R.var x (decode-encodeListArgTerm args i)
  decode-encodeTerm (R.con c args) i = R.con c (decode-encodeListArgTerm args i)
  decode-encodeTerm (R.def f args) i = R.def f (decode-encodeListArgTerm args i)
  decode-encodeTerm (R.lam v t) i = R.lam (decode-encodeVisibility v i) (decode-encodeAbsTerm t i)
  decode-encodeTerm (R.pat-lam cs args) i = R.pat-lam (decode-encodeListClause cs i) (decode-encodeListArgTerm args i)
  decode-encodeTerm (R.pi a b) i = R.pi (decode-encodeArgTerm a i) (decode-encodeAbsTerm b i)
  decode-encodeTerm (R.agda-sort s) i = R.agda-sort (decode-encodeSort s i)
  decode-encodeTerm (R.lit l) = refl
  decode-encodeTerm (R.meta x args) i = R.meta x (decode-encodeListArgTerm args i)
  decode-encodeTerm R.unknown = refl

  decode-encodeSort : (s : R.Sort) → decodeSort (encodeSort s) ≡ s
  decode-encodeSort (R.set t) i = R.set (decode-encodeTerm t i)
  decode-encodeSort (R.lit n) = refl
  decode-encodeSort (R.prop t) i = R.prop (decode-encodeTerm t i)
  decode-encodeSort (R.propLit n) = refl
  decode-encodeSort (R.inf n) = refl
  decode-encodeSort R.unknown = refl

  decode-encodePattern : (p : R.Pattern) → decodePattern (encodePattern p) ≡ p
  decode-encodePattern (R.con c ps) i = R.con c (decode-encodeListArgPattern ps i)
  decode-encodePattern (R.dot t) i = R.dot (decode-encodeTerm t i)
  decode-encodePattern (R.var x) = refl
  decode-encodePattern (R.lit l) = refl
  decode-encodePattern (R.proj f) = refl
  decode-encodePattern (R.absurd x) = refl

  decode-encodeClause : (c : R.Clause) → decodeClause (encodeClause c) ≡ c
  decode-encodeClause (R.clause tel ps t) i = R.clause (decode-encodeTelescope tel i) (decode-encodeListArgPattern ps i) (decode-encodeTerm t i)
  decode-encodeClause (R.absurd-clause tel ps) i = R.absurd-clause (decode-encodeTelescope tel i) (decode-encodeListArgPattern ps i)

  decode-encodeListArgTerm : (xs : List (R.Arg R.Term)) → decodeListArgTerm (encodeListArgTerm xs) ≡ xs
  decode-encodeListArgTerm [] = refl
  decode-encodeListArgTerm (x ∷ xs) i = decode-encodeArgTerm x i ∷ decode-encodeListArgTerm xs i

  decode-encodeArgTerm : (x : R.Arg R.Term) → decodeArgTerm (encodeArgTerm x) ≡ x
  decode-encodeArgTerm (R.arg i x) j = R.arg (decode-encodeArgInfo i j) (decode-encodeTerm x j)

  decode-encodeAbsTerm : (x : R.Abs R.Term) → decodeAbsTerm (encodeAbsTerm x) ≡ x
  decode-encodeAbsTerm (R.abs s x) i = R.abs s (decode-encodeTerm x i)

  decode-encodeListClause : (xs : List R.Clause) → decodeListClause (encodeListClause xs) ≡ xs
  decode-encodeListClause [] = refl
  decode-encodeListClause (x ∷ xs) i = decode-encodeClause x i ∷ decode-encodeListClause xs i

  decode-encodeListArgPattern : (xs : List (R.Arg R.Pattern)) → decodeListArgPattern (encodeListArgPattern xs) ≡ xs
  decode-encodeListArgPattern [] = refl
  decode-encodeListArgPattern (x ∷ xs) i = decode-encodeArgPattern x i ∷ decode-encodeListArgPattern xs i

  decode-encodeArgPattern : (x : R.Arg R.Pattern) → decodeArgPattern (encodeArgPattern x) ≡ x
  decode-encodeArgPattern (R.arg i x) j = R.arg (decode-encodeArgInfo i j) (decode-encodePattern x j)

  decode-encodeTelescope : (xs : R.Telescope) → decodeTelescope (encodeTelescope xs) ≡ xs
  decode-encodeTelescope [] = refl
  decode-encodeTelescope (x ∷ xs) i = decode-encodeTelEntry x i ∷ decode-encodeTelescope xs i

  decode-encodeTelEntry : (x : Σ String (λ _ → R.Arg R.Type)) → decodeTelEntry (encodeTelEntry x) ≡ x
  decode-encodeTelEntry (s , a) i = s , decode-encodeArgTerm a i

  decode-encodeArgInfo : (x : R.ArgInfo) → decodeArgInfo (encodeArgInfo x) ≡ x
  decode-encodeArgInfo (R.arg-info v m) i = R.arg-info (decode-encodeVisibility v i) (decode-encodeModality m i)

  decode-encodeModality : (x : R.Modality) → decodeModality (encodeModality x) ≡ x
  decode-encodeModality (R.modality r q) i = R.modality (decode-encodeRelevance r i) (decode-encodeQuantity q i)

  decode-encodeVisibility : (x : R.Visibility) → decodeVisibility (encodeVisibility x) ≡ x
  decode-encodeVisibility R.visible = refl
  decode-encodeVisibility R.hidden = refl
  decode-encodeVisibility R.instance′ = refl

  decode-encodeRelevance : (x : R.Relevance) → decodeRelevance (encodeRelevance x) ≡ x
  decode-encodeRelevance R.relevant = refl
  decode-encodeRelevance R.irrelevant = refl

  decode-encodeQuantity : (x : R.Quantity) → decodeQuantity (encodeQuantity x) ≡ x
  decode-encodeQuantity R.quantity-0 = refl
  decode-encodeQuantity R.quantity-ω = refl

mutual
  encode-decodeTerm : (t : CodeIx TermAtoms TermDesc (TermDesc termI)) → encodeTerm (decodeTerm t) ≡ t
  encode-decodeTerm (ν₂ ι₀ (atomIx x) (recIx args)) i =
    ν₂ ι₀ (atomIx x) (recIx (encode-decodeListArgTerm args i))
  encode-decodeTerm (ν₂ ι₁ (atomIx c) (recIx args)) i =
    ν₂ ι₁ (atomIx c) (recIx (encode-decodeListArgTerm args i))
  encode-decodeTerm (ν₂ ι₂ (atomIx f) (recIx args)) i =
    ν₂ ι₂ (atomIx f) (recIx (encode-decodeListArgTerm args i))
  encode-decodeTerm (ν₂ ι₃ (recIx v) (recIx t)) i =
    ν₂ ι₃ (recIx (encode-decodeVisibility v i)) (recIx (encode-decodeAbsTerm t i))
  encode-decodeTerm (ν₂ ι₄ (recIx cs) (recIx args)) i =
    ν₂ ι₄ (recIx (encode-decodeListClause cs i)) (recIx (encode-decodeListArgTerm args i))
  encode-decodeTerm (ν₂ ι₅ (recIx a) (recIx b)) i =
    ν₂ ι₅ (recIx (encode-decodeArgTerm a i)) (recIx (encode-decodeAbsTerm b i))
  encode-decodeTerm (ν₁ ι₆ (recIx s)) i =
    ν₁ ι₆ (recIx (encode-decodeSort s i))
  encode-decodeTerm (ν₁ ι₇ (atomIx l)) = refl
  encode-decodeTerm (ν₂ ι₈ (atomIx x) (recIx args)) i =
    ν₂ ι₈ (atomIx x) (recIx (encode-decodeListArgTerm args i))
  encode-decodeTerm (ν₀ ι₉) = refl

  encode-decodeSort : (s : CodeIx TermAtoms TermDesc (TermDesc sortI)) → encodeSort (decodeSort s) ≡ s
  encode-decodeSort (ν₁ ι₀ (recIx t)) i =
    ν₁ ι₀ (recIx (encode-decodeTerm t i))
  encode-decodeSort (ν₁ ι₁ (atomIx n)) = refl
  encode-decodeSort (ν₁ ι₂ (recIx t)) i =
    ν₁ ι₂ (recIx (encode-decodeTerm t i))
  encode-decodeSort (ν₁ ι₃ (atomIx n)) = refl
  encode-decodeSort (ν₁ ι₄ (atomIx n)) = refl
  encode-decodeSort (ν₀ ι₅) = refl

  encode-decodePattern : (p : CodeIx TermAtoms TermDesc (TermDesc patternI)) → encodePattern (decodePattern p) ≡ p
  encode-decodePattern (ν₂ ι₀ (atomIx c) (recIx ps)) i =
    ν₂ ι₀ (atomIx c) (recIx (encode-decodeListArgPattern ps i))
  encode-decodePattern (ν₁ ι₁ (recIx t)) i =
    ν₁ ι₁ (recIx (encode-decodeTerm t i))
  encode-decodePattern (ν₁ ι₂ (atomIx x)) = refl
  encode-decodePattern (ν₁ ι₃ (atomIx l)) = refl
  encode-decodePattern (ν₁ ι₄ (atomIx f)) = refl
  encode-decodePattern (ν₁ ι₅ (atomIx x)) = refl

  encode-decodeClause : (c : CodeIx TermAtoms TermDesc (TermDesc clauseI)) → encodeClause (decodeClause c) ≡ c
  encode-decodeClause (ν₃ ι₀ (recIx tel) (recIx ps) (recIx t)) i =
    ν₃ ι₀ (recIx (encode-decodeTelescope tel i)) (recIx (encode-decodeListArgPattern ps i)) (recIx (encode-decodeTerm t i))
  encode-decodeClause (ν₂ ι₁ (recIx tel) (recIx ps)) i =
    ν₂ ι₁ (recIx (encode-decodeTelescope tel i)) (recIx (encode-decodeListArgPattern ps i))

  encode-decodeListArgTerm : (xs : CodeIx TermAtoms TermDesc (TermDesc listArgTermI)) → encodeListArgTerm (decodeListArgTerm xs) ≡ xs
  encode-decodeListArgTerm (ν₀ ι₀) = refl
  encode-decodeListArgTerm (ν₂ ι₁ (recIx x) (recIx xs)) i =
    ν₂ ι₁ (recIx (encode-decodeArgTerm x i)) (recIx (encode-decodeListArgTerm xs i))

  encode-decodeArgTerm : (x : CodeIx TermAtoms TermDesc (TermDesc argTermI)) → encodeArgTerm (decodeArgTerm x) ≡ x
  encode-decodeArgTerm (ν₂ ι₀ (recIx i) (recIx x)) j =
    ν₂ ι₀ (recIx (encode-decodeArgInfo i j)) (recIx (encode-decodeTerm x j))

  encode-decodeAbsTerm : (x : CodeIx TermAtoms TermDesc (TermDesc absTermI)) → encodeAbsTerm (decodeAbsTerm x) ≡ x
  encode-decodeAbsTerm (ν₂ ι₀ (atomIx s) (recIx x)) i =
    ν₂ ι₀ (atomIx s) (recIx (encode-decodeTerm x i))

  encode-decodeListClause : (xs : CodeIx TermAtoms TermDesc (TermDesc listClauseI)) → encodeListClause (decodeListClause xs) ≡ xs
  encode-decodeListClause (ν₀ ι₀) = refl
  encode-decodeListClause (ν₂ ι₁ (recIx x) (recIx xs)) i =
    ν₂ ι₁ (recIx (encode-decodeClause x i)) (recIx (encode-decodeListClause xs i))

  encode-decodeListArgPattern : (xs : CodeIx TermAtoms TermDesc (TermDesc listArgPatternI)) → encodeListArgPattern (decodeListArgPattern xs) ≡ xs
  encode-decodeListArgPattern (ν₀ ι₀) = refl
  encode-decodeListArgPattern (ν₂ ι₁ (recIx x) (recIx xs)) i =
    ν₂ ι₁ (recIx (encode-decodeArgPattern x i)) (recIx (encode-decodeListArgPattern xs i))

  encode-decodeArgPattern : (x : CodeIx TermAtoms TermDesc (TermDesc argPatternI)) → encodeArgPattern (decodeArgPattern x) ≡ x
  encode-decodeArgPattern (ν₂ ι₀ (recIx i) (recIx x)) j =
    ν₂ ι₀ (recIx (encode-decodeArgInfo i j)) (recIx (encode-decodePattern x j))

  encode-decodeTelescope : (xs : CodeIx TermAtoms TermDesc (TermDesc telescopeI)) → encodeTelescope (decodeTelescope xs) ≡ xs
  encode-decodeTelescope (ν₀ ι₀) = refl
  encode-decodeTelescope (ν₂ ι₁ (recIx x) (recIx xs)) i =
    ν₂ ι₁ (recIx (encode-decodeTelEntry x i)) (recIx (encode-decodeTelescope xs i))

  encode-decodeTelEntry : (x : CodeIx TermAtoms TermDesc (TermDesc telEntryI)) → encodeTelEntry (decodeTelEntry x) ≡ x
  encode-decodeTelEntry (ν₂ ι₀ (atomIx s) (recIx a)) i =
    ν₂ ι₀ (atomIx s) (recIx (encode-decodeArgTerm a i))

  encode-decodeArgInfo : (x : CodeIx TermAtoms TermDesc (TermDesc argInfoI)) → encodeArgInfo (decodeArgInfo x) ≡ x
  encode-decodeArgInfo (ν₂ ι₀ (recIx v) (recIx m)) i =
    ν₂ ι₀ (recIx (encode-decodeVisibility v i)) (recIx (encode-decodeModality m i))

  encode-decodeModality : (x : CodeIx TermAtoms TermDesc (TermDesc modalityI)) → encodeModality (decodeModality x) ≡ x
  encode-decodeModality (ν₂ ι₀ (recIx r) (recIx q)) i =
    ν₂ ι₀ (recIx (encode-decodeRelevance r i)) (recIx (encode-decodeQuantity q i))

  encode-decodeVisibility : (x : CodeIx TermAtoms TermDesc (TermDesc visibilityI)) → encodeVisibility (decodeVisibility x) ≡ x
  encode-decodeVisibility (ν₀ ι₀) = refl
  encode-decodeVisibility (ν₀ ι₁) = refl
  encode-decodeVisibility (ν₀ ι₂) = refl

  encode-decodeRelevance : (x : CodeIx TermAtoms TermDesc (TermDesc relevanceI)) → encodeRelevance (decodeRelevance x) ≡ x
  encode-decodeRelevance (ν₀ ι₀) = refl
  encode-decodeRelevance (ν₀ ι₁) = refl

  encode-decodeQuantity : (x : CodeIx TermAtoms TermDesc (TermDesc quantityI)) → encodeQuantity (decodeQuantity x) ≡ x
  encode-decodeQuantity (ν₀ ι₀) = refl
  encode-decodeQuantity (ν₀ ι₁) = refl

encodeTermRoot : R.Term → RootCodeIx TermAtoms TermDesc (rootData termI)
encodeTermRoot t = rootDataIx (encodeTerm t)

decodeTermRoot : RootCodeIx TermAtoms TermDesc (rootData termI) → R.Term
decodeTermRoot (rootDataIx t) = decodeTerm t

decode-encodeTermRoot : (t : R.Term) → decodeTermRoot (encodeTermRoot t) ≡ t
decode-encodeTermRoot = decode-encodeTerm

encode-decodeTermRoot : (t : RootCodeIx TermAtoms TermDesc (rootData termI)) → encodeTermRoot (decodeTermRoot t) ≡ t
encode-decodeTermRoot (rootDataIx t) =
  cong rootDataIx (encode-decodeTerm t)

TermTypeNames : Fin 17 → String
TermTypeNames Fin.zero = "Term"
TermTypeNames (Fin.suc Fin.zero) = "Sort"
TermTypeNames (Fin.suc (Fin.suc Fin.zero)) = "Pattern"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc Fin.zero))) = "Clause"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))) = "ListArgTerm"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))) = "ArgTerm"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))) = "AbsTerm"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))) = "ListClause"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))) = "ListArgPattern"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))) = "ArgPattern"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))) = "Telescope"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))) = "TelEntry"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))) = "ArgInfo"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))) = "Modality"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))) = "Visibility"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))))) = "Relevance"
TermTypeNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))))) = "Quantity"

TermConstructorNames : Fin 17 → List String
TermConstructorNames Fin.zero =
  "var" ∷ "con" ∷ "def" ∷ "lam" ∷ "pat-lam" ∷ "pi" ∷ "agda-sort" ∷ "lit" ∷ "meta" ∷ "unknown" ∷ []
TermConstructorNames (Fin.suc Fin.zero) =
  "set" ∷ "lit" ∷ "prop" ∷ "propLit" ∷ "inf" ∷ "unknown" ∷ []
TermConstructorNames (Fin.suc (Fin.suc Fin.zero)) =
  "con" ∷ "dot" ∷ "var" ∷ "lit" ∷ "proj" ∷ "absurd" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc Fin.zero))) =
  "clause" ∷ "absurd-clause" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))) =
  "[]" ∷ "_∷_" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))) =
  "arg" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))) =
  "abs" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))) =
  "[]" ∷ "_∷_" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))) =
  "[]" ∷ "_∷_" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))) =
  "arg" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))) =
  "[]" ∷ "_∷_" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))) =
  "_,_" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))) =
  "arg-info" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))) =
  "modality" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))) =
  "visible" ∷ "hidden" ∷ "instance′" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))))) =
  "relevant" ∷ "irrelevant" ∷ []
TermConstructorNames (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))))) =
  "quantity-0" ∷ "quantity-ω" ∷ []

genericTerm : Generic TermAtoms R.Term
genericTerm =
  generic 17 TermDesc (rootData termI)
    TermTypeNames
    TermConstructorNames
    encodeTermRoot decodeTermRoot
    decode-encodeTermRoot encode-decodeTermRoot

TermConstructorNamesFit :
  (i : Fin 17) →
  ConstructorNamesFit
    (constructorsOf (TermDesc i))
    (TermConstructorNames i)
TermConstructorNamesFit Fin.zero =
  _∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ ([]ⁿ))))))))))
TermConstructorNamesFit (Fin.suc Fin.zero) =
  _∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ ([]ⁿ))))))
TermConstructorNamesFit (Fin.suc (Fin.suc Fin.zero)) =
  _∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ ([]ⁿ))))))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc Fin.zero))) =
  _∷ⁿ_ (_∷ⁿ_ ([]ⁿ))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))) =
  _∷ⁿ_ (_∷ⁿ_ ([]ⁿ))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))) =
  _∷ⁿ_ ([]ⁿ)
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))) =
  _∷ⁿ_ ([]ⁿ)
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))) =
  _∷ⁿ_ (_∷ⁿ_ ([]ⁿ))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))) =
  _∷ⁿ_ (_∷ⁿ_ ([]ⁿ))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))) =
  _∷ⁿ_ ([]ⁿ)
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))) =
  _∷ⁿ_ (_∷ⁿ_ ([]ⁿ))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))) =
  _∷ⁿ_ ([]ⁿ)
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))) =
  _∷ⁿ_ ([]ⁿ)
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))) =
  _∷ⁿ_ ([]ⁿ)
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))) =
  _∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ ([]ⁿ)))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero))))))))))))))) =
  _∷ⁿ_ (_∷ⁿ_ ([]ⁿ))
TermConstructorNamesFit (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc (Fin.suc Fin.zero)))))))))))))))) =
  _∷ⁿ_ (_∷ⁿ_ ([]ⁿ))

certifiedGenericTerm : CertifiedGeneric TermAtoms R.Term
certifiedGenericTerm =
  certifiedGeneric genericTerm TermConstructorNamesFit