{ 
x:Id. [T:Type]. (Normal(T) 
Normal(x : T)) }
{ Proof }
Definitions occuring in Statement :
normal-ds: Normal(ds),
normal-type: Normal(T),
fpf-single: x : v,
Id: Id,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
universe: Type
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
implies: P Q,
normal-ds: Normal(ds),
fpf-all: x
dom(f). v=f(x) P[x; v],
member: t T,
top: Top,
so_lambda: 
x.t[x],
fpf-single: x : v,
fpf-ap: f(x),
pi2: snd(t),
so_apply: x[s],
normal-type: Normal(T),
prop: 
Lemmas :
assert_witness,
fpf-dom_wf,
Id_wf,
id-deq_wf,
fpf-single_wf,
top_wf,
assert_wf,
normal-type_wf
\mforall{}x:Id. \mforall{}[T:Type]. (Normal(T) {}\mRightarrow{} Normal(x : T))
Date html generated:
2011_08_10-AM-08_12_55
Last ObjectModification:
2011_06_18-AM-08_27_53
Home
Index