have h_inductive (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)) (ih : motive idx.1 res) :
  motive (idx.1 + 1) (reduce_fold_fn assignment res c_arr[idx]) := reduce_fold_fn_preserves_induction_motive idx res ih
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
c_clause_rw : c.clause = c_arr.data
motive : Nat → ReduceResult (PosFin n) → Prop := reduce_postcondition_induction_motive c_arr assignment
h_base : motive 0 reducedToEmpty
h_inductive :
  ∀ (idx : Fin c_arr.size) (res : ReduceResult (PosFin n)),
    motive (↑idx) res → motive (↑idx + 1) (reduce_fold_fn assignment res c_arr[idx])
⊢ (Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToEmpty →
      incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      Array.foldl (reduce_fold_fn assignment) reducedToEmpty c_arr 0 = reducedToUnit l →
        ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l