---

{ Comm-output()  Type }

{ Proof }

---

Definitions occuring in Statement :  Comm-output: Comm-output(),  member: t  T,  universe: Type
Definitions :  token: "$token",  member: t  T,  equal: s = t,  function: x:A  B[x],  all: x:A. B[x],  PiDataVal: PiDataVal(),  tag-case: z:T,  Id: Id,  product: x:A  B[x],  labeled-graph: LabeledGraph(T),  Comm-state: Comm-state(),  Comm-output: Comm-output(),  universe: Type,  fpf: a:A fp-> B[a],  subtype: S  T,  subtype_rel: A r B,  implies: P  Q,  eclass: EClass(A[eo; e])
Lemmas :  member_wf,  Comm-state_wf,  labeled-graph_wf,  Id_wf,  tag-case_wf,  PiDataVal_wf

---

Comm-output()  \mmember{}  Type


Date html generated: 2010_08_27-PM-08_46_33
Last ObjectModification: 2010_04_27-PM-03_29_08

Home Index