Theorem: lrEndNodes (Bml/Tableau.lean)

State before:
LR : TNode
C : List TNode
ruleA : LocalRuleApp LR C
subTabs : (c : TNode) → c ∈ C → LocalTableau c
⊢ endNodesOf ⟨LR, fromRule ruleA subTabs⟩ =
    (List.map
        (fun x =>
          match x with
          | ⟨c, c_in⟩ => endNodesOf ⟨c, subTabs c c_in⟩)
        C.attach).join
Tactic:
simp only [endNodesOf]
State after:
no goals