Sugar for anonymous tuples and projecting away type parameters

It would be nice to have anonymous tuples as well as the ability to project away type parameter information. These came up for me as I tried to do a 'simple' example of showing that a theory of vectors was a monoid via a theory morphism. This requires sending `default::TYPE` to some type in `ThVect`. However, if one only is able to say `Vect(n)` for some `n`, then there doesn't exist a type for `default` to get mapped to!

```julia

using GATlab, GATlab.Stdlib

"""
A theory of vectors with elements of type `X` and type-level length information,
e.g. given a model with `X` mapping to `Symbol`, then [:a,:b,:c] is a Vect(3).

This has the intended semantics if ℕ really is the natural numbers, but this
would require a doctrine that can express sum types, which GATs cannot.
"""
@theory ThVect <: ThNatPlus begin
#########
# Types #
#########
X::TYPE
Vect(len::ℕ)::TYPE

#######################################################################
# Ability to forget/recover type information: should be autogenerated #
#######################################################################

Vect::TYPE # type of all vects, of any length. In bijection with ΣₙVect(n)
len(v::Vect)::ℕ

πVect(v::Vect(n))::Vect ⊣ [n::ℕ]
ιVect(v::Vect)::Vect(len(v))

len(πVect(v)) == n ⊣ [n::ℕ, v::Vect(n)]

ιVect(πVect(v)) == v ⊣ [n::ℕ, v::Vect(n)]
πVect(ιVect(v)) == v ⊣ [v::Vect]

###################################################
# Ability to tuple types: should be autogenerated #
###################################################

X_Vect(n::ℕ)::TYPE # type of (X,Vect(n)) pairs
mk_tup(x::X, v::Vect(n))::X_Vect(n) ⊣ [n::ℕ]
proj1(xv::X_Vect(n))::X ⊣ [n::ℕ]
proj2(xv::X_Vect(n))::Vect(n) ⊣ [n::ℕ]

proj1(mk_tup(x,y)) == x ⊣ [n::ℕ, x::X, y::Vect(n)]
proj2(mk_tup(x,y)) == y ⊣ [n::ℕ, x::X, y::Vect(n)]

##############
# Operations #
##############

empty()::Vect(Z())
concat(x::Vect(n), y::Vect(m))::Vect(n+m) ⊣ [(n,m)::ℕ]
pop(v::Vect(S(n)))::X_Vect(n) ⊣ [n::ℕ]
push(x::X, v::Vect(n))::Vect(S(n)) ⊣ [n::ℕ]

proj2(pop(push(x, v))) == v ⊣ [x::X, n::ℕ, v::Vect(n)]

concat(v, push(x,w)) == push(x, concat(v,w)) ⊣ [
(n,m)::ℕ,v::Vect(n),w::Vect(m), x::X] # push goes to end of list

end

@theorymap F(ThMonoid, ThVect) begin
default() => Vect
e() => πVect(empty())
(a⋅b) ⊣ [(a,b)::default] => πVect(concat(ιVect(a),ιVect(b)))
end
```

This is in the spirit of `struct` type sugar, which has very basic support (see NonStdlib's `ThPushout`),