rcases X with ⟨L, R, O⟩
case mp
X : TNode
X_is_consistent : consistent X
⊢ satisfiable X
case mp.mk.mk
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
X_is_consistent : consistent (L, R, O)
⊢ satisfiable (L, R, O)