Add the LazyTreeProofGenerator. (#5948)

Add the LazyTreeProofGenerator. (#5948)

This PR adds a new proof utility to construct tree-shaped proofs in a lazy fashion.
The LazyTreeProofGenerator is currently intended to be used for CAD proofs, where we need to construct proofs that consist of nested case-splits, but the exact split (in a form suitable for proof construction) is only known when the whole subtree is finished.
We thus store the proof in a tree structure similar to proof nodes, and transform the whole proof to a proper proof node once all data is available.