Feature: Syntax and delaborator for TypeVec and Fin2s

[alexkeizer]

Types like the following will occasionally show up in type errors, but are not particularly readable:

(Vec.append1 (Vec.append1 (Vec.append1 Vec.nil (Prj (Fin2.fs Fin2.fz))) (Prj Fin2.fz))
      (Comp (TypeFun.ofCurried (MvQPF.Arrow α)) (Vec.append1 Vec.nil (Prj (Fin2.fs Fin2.fz))))
      Fin2.fz

It would be nicer if we had syntax (and accompanying pretty printers!) for typevectors and Fin2s.
For example, we could use !![...] list notation, and &0, &1, etc.
Then, the above type could be pretty printed as:

!![MvQPF.Prj &1, MvQPF.Prj &0, Comp (TypeFun.ofCurried (MvQPF.Arrow α)) !![Prj &1]] &0

Making it much more obvious that the TypeVec is being indexed by the last Fin2.