ATruncType: added [contr_equiv_contr_contr], completing dependencies of [istrunc_trunctype].
Cleaned up auxiliary lemmas in TruncType.