{ PropRule 
' }
{ Proof }
Definitions occuring in Statement :
prop-rule: PropRule,
member: t T,
universe: Type
Definitions :
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
universe: Type,
prop-rule: PropRule,
name: Name,
prop: 
,
assert: 
b,
apply: f a,
list: type List,
not: 
A,
false: False,
void: Void,
less_than: a < b,
length: ||as||,
strong-subtype: strong-subtype(A;B),
ge: i 
j ,
le: A 
B,
cdv-types: cdv-types(dv),
bool: 
,
exists: 
x:A. B[x],
product: x:A 
B[x],
classderiv: ClassDerivation,
rec: rec(x.A[x]),
Id: Id,
atom: Atom$n,
hd: hd(l),
list_ind: list_ind def,
intensional-universe: IType,
set: {x:A| B[x]} ,
es-E-interface: E(X),
implies: P 
Q,
eclass: EClass(A[eo; e]),
subtype: S 
T,
all: 
x:A. B[x],
function: x:A 
B[x],
equal: s = t,
fpf: a:A fp-> B[a],
limited-type: LimitedType,
subtype_rel: A r B,
member: t T
Lemmas :
subtype_rel_wf,
limited-type_wf,
member_wf,
intensional-universe_wf,
Id_wf,
cdv-types_wf,
hd_wf,
assert_wf,
bool_wf,
name_wf,
classderiv_wf,
cdv-types-non-empty
PropRule \mmember{} \mBbbU{}'
Date html generated:
2010_08_30-AM-12_56_47
Last ObjectModification:
2010_08_23-PM-01_15_14
Home
Index