http://research.nuance.com/multiple-conclusion-linear-logic-cut-elimination-and-more/

So, can do something.
That's where we should move, I guess.

So, I kind of discovered that the stuff I'm doing with my Result class looks suspiciously close to linear logic, e.g., in LL we have !(A&B)≡!A⊗!B, and I have Good(a) <*> Good(b) == Good((a,b)).

Moving on.

Similarly, there's some connection between Good[Either[A,B]] and Good(a:A) orElse Good(b:B).

Actually, what I have, it seems to be a coaffine logic, but well, who cares right now. We will see.

"If Γ,Δ⊢Θ, then Γ,!A,Δ⊢Θ, for any A " maps to

Good(a) foreach (f()) is the same as f().

"If Γ,!A,!A,Δ⊢Θ, then Γ,!A,Δ⊢Θ" maps to
Good(Good(a)).flatten == Good(a)

Not everything works. But is not it weird.