Polynomial-time unary input length — proof internals

theorem Complexity.unaryLength_mem_FP_internal : (fun (x : List Bool) => List.replicate x.length true) ∈ FP

Internal proof that materializing unary input length is in FP.