rw [disEvalHT]
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w (dis (f :: X)) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1
case cons
W : Type
M : KripkeModel W
w : W
f : Formula
X : List Formula
IH : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f
⊢ evaluate M w f ∨ evaluate M w (dis X) ↔ ∃ f_1 ∈ f :: X, evaluate M w f_1