case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
i : Fin2 n
x : F α
x✝ : α i
⊢ x✝ ∈ supp x i ↔
    x✝ ∈ {u | ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ}
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
i : Fin2 n
x : F α
⊢ supp x i = {u | ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ}
ext
no goals
case h
n : ℕ
F : TypeVec n → Type u_1
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
i : Fin2 n
x : F α
x✝ : α i
⊢ x✝ ∈ supp x i ↔
    x✝ ∈ {u | ∀ (a : (P F).A) (f : MvPFunctor.B (P F) a ⟹ α), abs { fst := a, snd := f } = x → u ∈ f i '' univ}
apply mem_supp