(*Dummy theory to document dependencies *) WO2_AC16 = AC_Equiv + recfunAC16 + AC16_lemmas + Cardinal_aux