Theorem: unitClause_at_literal (Saturn/Clause.lean)

State before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ get' (unitClause n b k w) k w = some b
Tactic:
rw [unitClause, Vector.of_Fn'_get']
State after:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) k w = some b

State before:
n : ℕ
b : Bool
k : ℕ
w : k < n + 1
⊢ FinSeq.insert (some b) n k w (get' (contradiction n)) k w = some b
Tactic:
apply insert_at_focus
State after:
no goals