Theorem: Set.subset_univ (GMLInit/Data/Set/Subset.lean)

State before:
α : Sort u_1
s✝ t u s : Set α
⊢ s.Subset Set.univ
Tactic:
intro _ _
State after:
α : Sort u_1
s✝ t u s : Set α
x✝ : α
a✝ : x✝ ∈ s
⊢ x✝ ∈ Set.univ

State before:
α : Sort u_1
s✝ t u s : Set α
x✝ : α
a✝ : x✝ ∈ s
⊢ x✝ ∈ Set.univ
Tactic:
trivial
State after:
no goals