A-posteriori soundness condition for deep splitting
Status: open
Deep Target Splitting is justified because dist-arrow/dist-mu forward always holds, so reassembly of split pieces is ≡. The task (2026-05-31) is to proof-read the redesigned rule with deep splitting + an a-posteriori soundness condition and confirm the split pieces always reassemble to an equivalence, so soundness is preserved under the non-deterministic search.
What would settle it
A soundness proof for the redesigned cover rule that leans only on bidirectionality of dist-arrow/dist-mu, plus a termination argument on the msize measure.
Related
Deep Target Splitting · Distributivity Subtyping Laws