{ std-l2m() 
Id 
Message }
{ Proof }
Definitions occuring in Statement :
std-l2m: std-l2m(),
Message: Message,
Id: Id,
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,
Id: Id,
fpf: a:A fp-> B[a],
subtype: S T,
eclass: EClass(A[eo; e]),
implies: P 
Q,
es-E-interface: E(X),
atom: Atom$n,
product: x:A 
B[x],
exists: 
x:A. B[x],
nat: 
,
limited-type-level: limited-type-level{i:l}(n;T),
strong-subtype: strong-subtype(A;B),
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-l2m: std-l2m(),
MaAuto: Error :MaAuto,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
RepUR: Error :RepUR
Lemmas :
Id_wf,
Message_wf,
limited-type-level_wf,
nat_wf,
atom2_wf_limited,
limited-type_wf,
subtype_rel_wf,
intensional-universe_wf,
member_wf
std-l2m() \mmember{} Id {}\mrightarrow{} Message
Date html generated:
2010_08_27-PM-08_05_05
Last ObjectModification:
2010_06_09-PM-11_59_43
Home
Index