---

Step * of Lemma local-class-ap-member

∀[Info,A,T:Type]. ∀[X:T ─→ EClass(A)]. ∀[prog:∀x:T. LocalClass(X x)]. ∀[x:T].  (prog x ∈ LocalClass(X x))
BY
{ Auto }

---

Latex:


\mforall{}[Info,A,T:Type].  \mforall{}[X:T  {}\mrightarrow{}  EClass(A)].  \mforall{}[prog:\mforall{}x:T.  LocalClass(X  x)].  \mforall{}[x:T].
    (prog  x  \mmember{}  LocalClass(X  x))


By

Auto

---

Home Index