case mk
α✝ : Type u_1
A✝ : α✝ → PSet
i : Type (mk α✝ A✝)
⊢ Func (mk α✝ A✝) i ∈ mk α✝ A✝
x : PSet
i : Type x
⊢ Func x i ∈ x
cases x
no goals
case mk
α✝ : Type u_1
A✝ : α✝ → PSet
i : Type (mk α✝ A✝)
⊢ Func (mk α✝ A✝) i ∈ mk α✝ A✝
apply Mem.mk