Order property assignments

[ScriptRaccoon]

When manually assigning properties to categories, it often happens that one proof refers to an assignment made earlier in the file. However, before this PR, manually assigned properties were listed alphabetically. This could be confusing, since the proofs could not be read from top to bottom in their natural order. It could also result in less important properties being listed first.

This PR resolves the issue by assigning an autoincrementing ID to every property assignment, whether manual or deduced. Previously, the table used a composite primary key consisting of category ID and property ID. Displayed properties are now ordered by ID and therefore appear in the same order as in the file where they are assigned. This also allows contributors to deliberately choose which properties should be shown first.

The position column previously used for deduced properties is now redundant. Deduced properties are still displayed in a logical order, unaffected by this PR, and their order cannot be influenced by contributors.

The same remarks apply to assignments of properties to functors.

Before

This is from the walking_fork page. It is weird that "cofiltered-limit-stable epimorphisms" appears first.

After

This has now the same order as in the file:

(
	'walking_fork',
	'finite',
	TRUE,
	'This is trivial.'
),
(
	'walking_fork',
	'small',
	TRUE,
	'This is trivial.'
),
...

Before

This is taken from the Top page. It is weird that "locally small" is quite at the bottom, while "coregular" is quite at the top (among other things).

After