Theorem: contradiction_is_false (Saturn/Clause.lean)

State before:
n : ℕ
⊢ ∀ (valuation : Valuation n), ¬ClauseSat (contradiction n) valuation
Tactic:
intro valuation ⟨k, ⟨b, p⟩⟩
State after:
n : ℕ
valuation : Valuation n
k : ℕ
b : k < n
p : VarSat (Vector.get (contradiction n) { val := k, isLt := b }) (Vector.get valuation { val := k, isLt := b })
⊢ False

State before:
n : ℕ
valuation : Valuation n
k : ℕ
b : k < n
p : VarSat (Vector.get (contradiction n) { val := k, isLt := b }) (Vector.get valuation { val := k, isLt := b })
⊢ False
Tactic:
simp [get_contradiction, VarSat] at p
State after:
no goals