{ std-n2m() 
Message }
{ Proof }
Definitions occuring in Statement :
std-n2m: std-n2m(),
Message: Message,
nat: ,
member: t T,
function: x:A B[x]
Definitions :
member: t T,
equal: s = t,
set: {x:A| B[x]} ,
limited-type: LimitedType,
intensional-universe: IType,
subtype_rel: A 
r B,
function: x:A B[x],
all: 
x:A. B[x],
universe: Type,
implies: P 
Q,
false: False,
not: 
A,
le: A 
B,
int: 
,
nat: ,
fpf: a:A fp-> B[a],
subtype: S T,
eclass: EClass(A[eo; e]),
es-E-interface: E(X),
product: x:A 
B[x],
exists: 
x:A. B[x],
strong-subtype: strong-subtype(A;B),
real: 
,
grp_car: Error :grp_car,
pair: <a, b>,
atom: Atom,
list: type List,
nil: [],
pMsg: pMsg(P.M[P]),
mData: mData,
name: Name,
Message: Message,
l_member: (x l),
lambda: 
x.A[x],
std-n2m: std-n2m(),
MaAuto: Error :MaAuto,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
RepUR: Error :RepUR
Lemmas :
nat_wf,
Message_wf,
int_wf_limited,
limited-type_wf,
subtype_rel_wf,
intensional-universe_wf,
member_wf
std-n2m() \mmember{} \mBbbN{} {}\mrightarrow{} Message
Date html generated:
2010_08_27-PM-08_05_01
Last ObjectModification:
2010_06_09-PM-11_58_05
Home
Index