Nuprl Lemma : eq_id_wf
[a,b:Id]. (a = b 
)
Proof not projected
Definitions occuring in Statement :
eq_id: a = b,
Id: Id,
bool: ,
uall: [x:A]. B[x],
member: t T
Definitions :
eq_id: a = b,
member: t T,
uall: [x:A]. B[x],
so_lambda: 
x.t[x],
deq: EqDecider(T),
so_apply: x[s]
Lemmas :
Id_wf,
assert_wf,
equal_wf,
iff_wf,
all_wf,
bool_wf,
subtype_rel_set_simple,
id-deq_wf
\mforall{}[a,b:Id]. (a = b \mmember{} \mBbbB{})
Date html generated:
2012_01_23-AM-11_52_53
Last ObjectModification:
2011_12_09-PM-07_33_07
Home
Index