aesop
L R : Finset Formula
C : List TNode
snd✝ : Finset Formula
a✝ : List (Finset Formula)
rule : LocalRule (∅, snd✝) (List.map (fun res => (∅, res)) a✝)
hC : C = applyLocalRule rule (L, R)
preproof : ∅ ⊆ L ∧ snd✝ ⊆ R
orule : OneSidedLocalRule snd✝ a✝
ruleApp : LocalRuleApp (L, R) C
hmyrule : ruleApp = LocalRuleApp.mk (List.map (fun res => (∅, res)) a✝) ∅ snd✝ rule preproof
rule_is_right : rule = LocalRule.oneSidedR orule
⊢ ∀ c ∈ C, c.1 = L
no goals