Nuprl Lemma : eq_id_self
[a:Id]. (a = a ~ tt)
Proof not projected
Definitions occuring in Statement :
eq_id: a = b,
Id: Id,
btrue: tt,
uall: [x:A]. B[x],
sqequal: s ~ t
Definitions :
member: t 
T,
eq_id: a = b,
uall: [x:A]. B[x],
guard: {T},
implies: P 
Q,
all: x:A. B[x],
eqof: eqof(d),
uimplies: b supposing a,
sq_type: SQType(T)
Lemmas :
btrue_wf,
id-deq_wf,
Id_wf,
eqof_eq_btrue,
bool_subtype_base,
bool_wf,
subtype_base_sq
\mforall{}[a:Id]. (a = a \msim{} tt)
Date html generated:
2012_01_23-AM-11_52_56
Last ObjectModification:
2011_12_09-PM-07_20_48
Home
Index