intro W M w
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
⊢ Con X≡discon B
X : List Formula
B : List (List Formula)
lr : OneSidedLocalRule X B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con X) ↔ evaluate M w (discon B)