simp only [reduce_postcondition_induction_motive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall,
  forall_const, false_implies, implies_true, and_true, motive]
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
⊢ motive 0 reducedToEmpty
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
⊢ ∀ (p : PosFin n → Bool), (∀ (i : Fin c_arr.size), ↑i < 0 → ¬(p ⊨ c_arr[↑i])) ∨ ¬(p ⊨ assignment)