{ Comm-state() 
Type }
{ Proof }
Definitions occuring in Statement :
Comm-state: Comm-state(),
member: t T,
universe: Type
Definitions :
universe: Type,
member: t T,
nat: 
,
equal: s = t,
bool: 
,
product: x:A 
B[x],
function: x:A 
B[x],
all: 
x:A. B[x],
pi_prefix: pi_prefix(),
list: type List,
Id: Id,
lambda: 
x.A[x],
so_lambda: 
x.t[x],
fpf: a:A fp-> B[a],
Comm-state: Comm-state(),
subtype: S 
T,
subtype_rel: A r B,
implies: P 
Q,
eclass: EClass(A[eo; e]),
MaAuto: Error :MaAuto
Lemmas :
member_wf,
fpf_wf,
Id_wf,
pi_prefix_wf,
bool_wf,
nat_wf
Comm-state() \mmember{} Type
Date html generated:
2010_08_27-PM-08_46_30
Last ObjectModification:
2010_03_29-PM-12_33_53
Home
Index