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