case inr canApplyRule =>
  rw [not_not] at canApplyRule
  rcases canApplyRule with ⟨LCond, RCond, C, lr_exists, preconL, preconR⟩
  cases' lr_exists with lr
  constructor
  apply LocalTableau.fromRule
  apply LocalRuleApp.mk C LCond RCond lr ⟨preconL, preconR⟩
  use applyLocalRule lr (LR.1, LR.2)
  rfl
  intro c c_in
  let ruleA := @LocalRuleApp.mk LR.1 LR.2 (applyLocalRule lr (LR.1, LR.2)) _ LCond RCond lr rfl ⟨preconL, preconR⟩
  have := localRuleAppDecreasesLength ruleA c c_in
  apply Classical.choice (existsLocalTableauFor c)
LR : TNode
canApplyRule : ¬¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
no goals