---

Step * 2 of Lemma parameter-class-val

.....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) ∈ ℙ
BY
{ (InstLemma `es-parameter-class_wf` [⌈Info⌉;⌈es⌉;⌈X⌉;⌈T⌉;⌈p⌉]⋅ THEN Auto) }

---

Latex:


.....wf..... 
1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  T  :  Type
5.  p  :  Id  {}\mrightarrow{}  T
6.  e  :  E
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  Parameter(p;X)  \mmember{}  \mBbbP{}


By

(InstLemma  `es-parameter-class\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index