Nuprl Lemma : dec_eq_type_wf
T:Type. (dec_eq_type(T) 
)
Proof
Definitions occuring in Statement :
dec_eq_type: dec_eq_type(T),
prop: ,
all: x:A. B[x],
member: t T,
universe: Type
Definitions :
all: x:A. B[x],
member: t T,
dec_eq_type: dec_eq_type(T),
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
so_apply: x[s]
Lemmas :
all_wf,
decidable_wf,
equal_wf
\mforall{}T:Type. (dec\_eq\_type(T) \mmember{} \mBbbP{})
Date html generated:
2013_03_20-AM-09_45_38
Last ObjectModification:
2012_12_07-AM-00_12_37
Home
Index