simp only [not_nonempty_iff, not_isEmpty_iff, not_exists, not_forall, exists_prop, Nonempty.forall]
LR : TNode
⊢ (¬let LR := LR;
      ¬let LR := LR;
        Nonempty (ClosedTableau LoadHistory.nil LR)) →
    ¬satisfiable LR
LR : TNode
⊢ ClosedTableau LoadHistory.nil LR → ¬satisfiable LR