{ 
[S:Type]. [F:S 
Type]. m:S 
(F m) 
Void supposing S Void }
{ Proof }
Definitions occuring in Statement :
ext-eq: A B,
uimplies: b supposing a,
uall: [x:A]. B[x],
apply: f a,
function: x:A B[x],
product: x:A B[x],
void: Void,
universe: Type
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
ext-eq: A B,
and: P 
Q,
member: t 
T,
cand: A c B,
all: x:A. B[x],
implies: P 
Q
Lemmas :
subtype_rel_wf,
uall_wf,
uiff_inversion,
member_wf,
ext-eq_inversion
\mforall{}[S:Type]. \mforall{}[F:S {}\mrightarrow{} Type]. m:S \mtimes{} (F m) \mequiv{} Void supposing S \mequiv{} Void
Date html generated:
2011_08_17-PM-06_58_31
Last ObjectModification:
2011_06_18-PM-12_37_28
Home
Index