involutions are equivalences
some extra lemmas about BAut(X)
better names for some induction principles