case h
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.112962
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ pi ∅ s ↔ x✝ ∈ univ
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.112962
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : (i : ι) → Set (α i)
⊢ pi ∅ s = univ
ext
no goals
case h
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.112962
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ pi ∅ s ↔ x✝ ∈ univ
simp [pi]