Use structure instead of inductive where possible

[tothtamas28]

We can map constructors whose arguments are cells to structure instead of inductive, since in this case the cell names give reasonable and unique names for fields. For example:

<generatedTop>
    <k></k>
    <generatedCounter></generatedCounter>
</generatedTop>

can become

structure SortGeneratedTopCell where
  «<generatedTop>» :: (k : SortK) (generatedCounter : SortGeneratedCounterCell)

or

structure SortGeneratedTopCell where
  mk :: (k : SortK) (generatedCounter : SortGeneratedCounterCell)

or simply

structure SortGeneratedTopCell where
  k : SortK
  generatedCounter : SortGeneratedCounterCell

[JuanCoRo]

I like the third option better! But might be a bit trickier to implement?

[tothtamas28]

I like the third option better!

Me too. Semantically, it is actually equivalent to the second option, but reads nicer.