Remove useless lemma
Object notation now uses init and update

Hence the order in which the labels are given doesn't have to be the
same than in the type and looping methods may be omitted.