theorem
proved
bpow_bool_constraints_iff_active_unit_under_passive_down_roles
show as:
bpow_bool_constraints_iff_active_unit_under_passive_down_roles