{ 
[m:Message]. (msg-body(m) 
msg-type(m)) }
{ Proof }
Definitions occuring in Statement :
msg-type: msg-type(msg),
msg-body: msg-body(msg),
Message: Message,
uall: [x:A]. B[x],
member: t T
Definitions :
Message: Message,
msg-body: msg-body(msg),
msg-type: msg-type(msg),
equal: s = t,
member: t T,
function: x:A 
B[x],
all: x:A. B[x],
axiom: Ax,
isect: 
x:A. B[x],
uall: [x:A]. B[x],
RepUR: Error :RepUR,
Auto: Error :Auto,
THENA: Error :THENA,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic,
mData: mData,
pMsg: pMsg(P.M[P]),
pi2: snd(t),
product: x:A 
B[x],
name: Name,
so_lambda: 
x.t[x],
lambda: x.A[x],
universe: Type
Lemmas :
pi2_wf,
name_wf,
Message_wf
\mforall{}[m:Message]. (msg-body(m) \mmember{} msg-type(m))
Date html generated:
2011_08_17-PM-03_59_10
Last ObjectModification:
2011_05_13-PM-04_59_46
Home
Index