intro p
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)
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)