https://github.com/leanprover/cslib/blob/03c480f0c4fe2c7b6e07512d064d7b9d57f12ae7/Cslib/Logics/LinearLogic/CLL/MProof.lean#L22