Theorem: clauseContains_implies_clauseContains_beyond (Saturn/Containment.lean)

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

State before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : cl1⊇cl2
k : ℕ
kw : k < n
a✝ : m ≤ k
b : Bool
⊢ get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
exact h k kw b
State after:
no goals