---

Step * of Lemma parameter-class-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[T:Type]. ∀[p:Id ─→ T]. ∀[e:E].
  Parameter(p;X)(e) = (p loc(e)) ∈ T supposing ↑e ∈b Parameter(p;X)
BY
{ (BasicUniformUnivCD Auto THEN D 0) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. T : Type
5. p : Id ─→ T
6. e : E
7. ↑e ∈b Parameter(p;X)
⊢ Parameter(p;X)(e) = (p loc(e)) ∈ T

2
.....wf..... 
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. T : Type
5. p : Id ─→ T
6. e : E
⊢ ↑e ∈b Parameter(p;X) ∈ ℙ

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[T:Type].  \mforall{}[p:Id  {}\mrightarrow{}  T].  \mforall{}[e:E].
    Parameter(p;X)(e)  =  (p  loc(e))  supposing  \muparrow{}e  \mmember{}\msubb{}  Parameter(p;X)


By

(BasicUniformUnivCD  Auto  THEN  D  0)

---

Home Index