{ E#Rule 
' }
{ Proof }
Definitions occuring in Statement :
esharp-rule: E#Rule,
member: t T,
universe: Type
Definitions :
CollapseTHEN: Error :CollapseTHEN,
universe: Type,
MaAuto: Error :MaAuto,
esharp-rule: E#Rule,
expression: Expression,
name: Name,
prop: 
,
assert: 
b,
apply: f a,
list: type List,
strong-subtype: strong-subtype(A;B),
bool: 
,
exists: 
x:A. B[x],
product: x:A 
B[x],
Id: Id,
atom: Atom$n,
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,
assert_wf,
bool_wf,
name_wf,
expression_wf
E\#Rule \mmember{} \mBbbU{}'
Date html generated:
2010_08_30-AM-12_58_29
Last ObjectModification:
2010_08_23-PM-01_23_00
Home
Index