case inl canApplyRule =>
  constructor
  apply LocalTableau.fromSimple
  by_contra hyp
  have := notSimpleThenLocalRule hyp
  aesop
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
no goals