Polynomial-time pairing with the original input — proof internals

theorem Complexity.mem_FP_pairWithInput_internal {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => pair (f x) x) ∈ FP

Internal closure of FP under x ↦ pair (f x) x.