---

{ Kind  Type }

{ Proof }

---

Definitions occuring in Statement :  Kind: Kind,  member: t  T,  universe: Type
Definitions :  tactic: Error :tactic,  Kind: Kind,  union: left + right,  IdLnk: IdLnk,  all: x:A. B[x],  function: x:A  B[x],  equal: s = t,  member: t  T,  Id: Id,  product: x:A  B[x]
Lemmas :  Id_wf,  IdLnk_wf

---

Kind  \mmember{}  Type


Date html generated: 2010_08_26-PM-11_32_37
Last ObjectModification: 2009_10_14-PM-01_22_41

Home Index