Metatheory: use Fin instead of nested Maybe for representing variables

[basetunnel]

This changes the representation of variables in Untyped syntax to Fin n (see Untyped.lagda.md). The current AST type is parametrised by X : Set for variables, meant to be instantiated to Maybe (Maybe (... ⊥)), i.e. something isomorphic to Fin n. This underconstrained definition led to several work-arounds when @ramsay-t was working on the certifier.

The original motivation for using Maybe was to accomodate for an early version of agda2hs, but the metatheory is actually compiled using the MAlonzo backend nowadays.

Resulting simplifications:

• No more need to parametrise definitions by DecEq instances to compare variables in decision procedures (see e.g. UntypedTranslation.lagda.md)
• Many uses of Set₁ can now simply be Set
• Terms are now indexed by a natural number to represent the amount of variables that are in scope, e.g. 2 ⊢ instead of (Maybe (Maybe ⊥)) ⊢
• {-# OPTIONS --injective-type-constructors #-} is not needed anymore

[ana-pantilie]

Nice! I think you need to somehow restart CI since it timed-out. If CI is green, I think we can merge it.