Theorem: extracted_2 (FOL/Parsing/DFT.lean)

State before:
α : Type
ws xs ys zs : List α
x : α
h1 : ws ++ ys ⊆ zs
h2 : x :: xs ⊆ zs
⊢ x :: ys ⊆ zs
Tactic:
simp at *
State after:
α : Type
ws xs ys zs : List α
x : α
h1 : ws ⊆ zs ∧ ys ⊆ zs
h2 : x ∈ zs ∧ xs ⊆ zs
⊢ x ∈ zs ∧ ys ⊆ zs

State before:
α : Type
ws xs ys zs : List α
x : α
h1 : ws ⊆ zs ∧ ys ⊆ zs
h2 : x ∈ zs ∧ xs ⊆ zs
⊢ x ∈ zs ∧ ys ⊆ zs
Tactic:
tauto
State after:
no goals