Primary-input projection circuits -- proof internals

theorem Complexity.Circuit.eval_projectInputs_internal {N M : ℕ} [NeZero N] [NeZero M] (mapInput : Fin M → Fin N) (input : BitString N) : (projectInputs mapInput).eval input = input ∘ mapInput