have c_clause_rw : c.clause = c_arr.data := rfl
n : Nat
c : DefaultClause n
assignment : Array Assignment
c_arr : Array (Literal (PosFin n)) := { data := c.clause }
⊢ (c.reduce assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      c.reduce assignment = 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
⊢ (c.reduce assignment = reducedToEmpty → incompatible (PosFin n) c assignment) ∧
    ∀ (l : Literal (PosFin n)),
      c.reduce assignment = reducedToUnit l → ∀ (p : PosFin n → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l