{ pDVfire() 
PiDataVal() }
{ Proof }
Definitions occuring in Statement :
pDVfire: pDVfire(),
PiDataVal: PiDataVal(),
member: t T
Definitions :
equal: s = t,
member: t T,
function: x:A 
B[x],
all: 
x:A. B[x],
name: Name,
product: x:A 
B[x],
pi_prefix: pi_prefix(),
list: type List,
universe: Type,
nat: 
,
Id: Id,
union: left + right,
unit: Unit,
it: 
,
inl: inl x ,
inr: inr x ,
pDVfire: pDVfire(),
PiDataVal: PiDataVal()
Lemmas :
it_wf,
unit_wf,
Id_wf,
nat_wf,
pi_prefix_wf,
name_wf
pDVfire() \mmember{} PiDataVal()
Date html generated:
2010_08_27-PM-08_42_44
Last ObjectModification:
2010_04_23-AM-11_30_42
Home
Index