let motive := reduce_postcondition_induction_motive c_arr assignment
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
⊢ (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
⊢ (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