use head
case inl
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : Evaluate (M, w) head
⊢ ∃ φ ∈ head :: tail, Evaluate (M, w) φ
case h
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : Evaluate (M, w) (bigDis tail) → ∃ φ ∈ tail, Evaluate (M, w) φ
satDis : Evaluate (M, w) (bigDis (head :: tail))
h✝ : Evaluate (M, w) head
⊢ head ∈ head :: tail ∧ Evaluate (M, w) head