{ 
[x:Knd]. [T:Type]. Normal(x : T) supposing Dec(T) }
{ Proof }
Definitions occuring in Statement :
normal-da: Normal(da),
fpf-single: x : v,
Knd: Knd,
decidable: Dec(P),
uimplies: b supposing a,
uall: [x:A]. B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
normal-da: Normal(da),
member: t 
T,
true: True,
prop: 
Lemmas :
decidable_wf,
Knd_wf
\mforall{}[x:Knd]. \mforall{}[T:Type]. Normal(x : T) supposing Dec(T)
Date html generated:
2011_08_10-AM-08_13_00
Last ObjectModification:
2011_06_18-AM-08_27_58
Home
Index