unfold bigDis
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
⊢ Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
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
⊢ Evaluate (M, w) head ∨
    Evaluate (M, w)
      (match tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)