Theorem: clauseContains_beyond_zero_implies_contains (Saturn/Containment.lean)

State before:
n : ℕ
cl1 cl2 : Clause n
⊢ clauseContainsTail cl1 cl2 zero → cl1⊇cl2
Tactic:
intro h k kw b
State after:
n : ℕ
cl1 cl2 : Clause n
h : clauseContainsTail cl1 cl2 zero
k : ℕ
kw : k < n
b : Bool
⊢ get' cl2 k kw = some b → get' cl1 k kw = some b

State before:
n : ℕ
cl1 cl2 : Clause n
h : clauseContainsTail cl1 cl2 zero
k : ℕ
kw : k < n
b : Bool
⊢ get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
exact h k kw (Nat.zero_le _) b
State after:
no goals