Nuprl Lemma : normal-ds-single
∀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
Lemmas :
assert_wf,
fpf-dom_wf,
Id_wf,
id-deq_wf,
fpf-single_wf,
top_wf,
normal-type_wf
\mforall{}x:Id. \mforall{}[T:Type]. (Normal(T) {}\mRightarrow{} Normal(x : T))
Date html generated:
2015_07_17-AM-11_18_28
Last ObjectModification:
2015_01_28-AM-07_35_03
Home
Index