---

Step * of Lemma section-iota_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[I:fset(ℕ)]. ∀[rho:Gamma(I)]. ∀[a:A(rho)]. ∀[psi:𝔽(I)].
  (section-iota(Gamma;A;I;rho;a) ∈ {I,psi ⊢ _:((A)<rho>)iota})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[rho:Gamma(I)].  \mforall{}[a:A(rho)].  \mforall{}[psi:\mBbbF{}(I)].
    (section-iota(Gamma;A;I;rho;a)  \mmember{}  \{I,psi  \mvdash{}  \_:((A)<rho>)iota\})


By

---

Latex:
ProveWfLemma

---

Home Index