{ 0 
Pi_term }
{ Proof }
Definitions occuring in Statement :
pizero: 0,
pi_term: Pi_term,
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],
union: left + right,
pi_prefix: pi_prefix(),
universe: Type,
unit: Unit,
rec: rec(x.A[x]),
it: 
,
inl: inl x ,
eclass: EClass(A[eo; e]),
subtype_rel: A 
r B,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
decision: Decision,
pizero: 0,
pi_term: Pi_term
Lemmas :
member_wf,
it_wf,
unit_wf,
pi_prefix_wf,
name_wf
0 \mmember{} Pi\_term
Date html generated:
2010_08_27-PM-08_36_59
Last ObjectModification:
2010_02_11-PM-06_47_48
Home
Index