trans-2 -> trans-diag
Add ap2.
More definitional equalities in HLevelBis.