 Predicate prefix-suffix reconstruction

Concatenating the initial list prefix accepted by a predicate with the remaining list suffix reconstructs the input, provided every test reached before the first false result terminates. Prove the finite case by structural induction: a true test copies the head, and a false test returns the untouched list suffix. An undefined reached test is an obstruction because reconstruction loses an exposed cons cell. An infinite all-true list prefix can still reconstruct the input, since list concatenation never demands its second argument there.