Theorem: clauseContains_trans (Saturn/Containment.lean)

State before:
n : ℕ
cl1 cl2 cl3 : Clause n
⊢ cl1⊇cl2 → cl2⊇cl3 → cl1⊇cl3
Tactic:
intro hyp1 hyp2  k w b dHyp
State after:
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl1 k w = some b

State before:
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl1 k w = some b
Tactic:
apply hyp1
State after:
case a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl2 k w = some b

State before:
case a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl2 k w = some b
Tactic:
apply hyp2
State after:
case a.a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl3 k w = some b

State before:
case a.a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl3 k w = some b
Tactic:
apply dHyp
State after:
no goals