Constant and primary-input source circuits -- proof internals

theorem Complexity.Circuit.eval_inputSources_internal {inputWidth outputWidth : ℕ} [NeZero inputWidth] [NeZero outputWidth] (sources : Fin outputWidth → InputSource inputWidth) (input : BitString inputWidth) : (inputSources sources).eval input = fun (output : Fin outputWidth) => (sources output).eval input