NB: several of the above functions come with
..._norm variants
that expect reduced arguments and return reduced results.
TODO : also speak of specifications via Qcanon ...
NB: do not add
spec_0 in the autorewrite database. Otherwise,
after instanciation in BigQ, this lemma become convertible to 0=0,
and autorewrite loops. Idem for
spec_1 and
spec_m1
Morphisms