Auxiliary lemmas suitable for upstream

This index aggregates small auxiliary results that are not specific to Boolean functions and could plausibly live in Mathlib.