constructor
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ (reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty →
      ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)) ∧
    ∀ (a : PosFin n) (b : Bool),
      reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)
case left
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ reduce_fold_fn assignment res c_arr[↑idx] = reducedToEmpty →
    ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < ↑idx + 1 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)

case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
⊢ ∀ (a : PosFin n) (b : Bool),
    reduce_fold_fn assignment res c_arr[↑idx] = reducedToUnit (a, b) →
      ∀ (p : PosFin n → Bool), p ⊨ assignment → ∀ (x : Fin c_arr.size), ↑x < ↑idx + 1 → p ⊨ c_arr[↑x] → p ⊨ (a, b)