Kernel: Cut Proof Checking Fix

[sankalpgambhir]

Fixes a soundness bug in the kernel in the proof checking for the Cut proof step

Consider the following instance of Cut:

S1: A |- B, C     S2: C, D |- E
-------------------------------- Cut: wrt C
       S3: A, D |- B, E

where C ~ D, and A !~ D in ortholattices.

The (previous) Cut implementation would attempt the following check:

isSameSetUnderOL(
     {A, D} // from the conclusion: S3.LHS
     {A} union {C, D}.filterNot(_ ~ C) // from the premises:  S1.LHS U (S2.RHS / cutPivot)
)

However, {C, D}.filterNot(_ ~ C) = {}, so it is checking whether {A, D} = {A} under OL, but a counterpart for D is not found on the right. This filtering is too excessive.

We now perform a more permissive check:

isSameSetUnderOL(
     {A, D} + C // from the conclusion: S3.LHS + cutPivot
     {A} union {C, D} // from the premises:  S1.LHS U S2.RHS
)

which performs the 'correct' check, but the duplication C-equivalent formulas in the conclusion. However, this is still supported by our interpretation of sequent calculus.