unfold bigDis
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w) (bigDis (head :: tail)) ↔ Evaluate (M, w) head ∨ Evaluate (M, w) (bigDis tail)
W : Type
M : KripkeModel W
w : W
head : Formula
tail : List Formula
ih : (∃ φ ∈ tail, Evaluate (M, w) φ) → Evaluate (M, w) (bigDis tail)
satOne : ∃ φ ∈ head :: tail, Evaluate (M, w) φ
⊢ Evaluate (M, w)
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest) ↔
    Evaluate (M, w) head ∨
      Evaluate (M, w)
        (match tail with
        | [] => ⊥
        | [f] => f
        | f :: rest => f⋁bigDis rest)