repair use of total2 after update to Foundations

Voevodsky has removed various canonical structure declarations from
the Foundations, so we start to repair the proofs here which have
broken as a result.  The work is not yet complete.