unfold inconsistent
LR : TNode
⊢ (¬let LR := LR;
      ¬inconsistent LR) →
    ¬satisfiable LR
LR : TNode
⊢ (¬let LR := LR;
      ¬let LR := LR;
        Nonempty (ClosedTableau LoadHistory.nil LR)) →
    ¬satisfiable LR