Theorem: not_sat_and_unsat (Saturn/Core.lean)

State before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
⊢ IsSat clauses → IsUnSat clauses → False
Tactic:
intro ⟨v, p⟩ h2
State after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
v : Valuation (n + 1)
p :
  ∀ (p : ℕ) (pw : p < num_clauses),
    ∃ k kw,
      Vector.get (Vector.get clauses { val := p, isLt := pw }) { val := k, isLt := kw } =
        some (Vector.get v { val := k, isLt := kw })
h2 : IsUnSat clauses
⊢ False

State before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
v : Valuation (n + 1)
p :
  ∀ (p : ℕ) (pw : p < num_clauses),
    ∃ k kw,
      Vector.get (Vector.get clauses { val := p, isLt := pw }) { val := k, isLt := kw } =
        some (Vector.get v { val := k, isLt := kw })
h2 : IsUnSat clauses
⊢ False
Tactic:
exact h2 v p
State after:
no goals