Nuprl Lemma : assert-eq-id
[a,b:Id]. uiff(
a = b;a = b)
Proof not projected
Definitions occuring in Statement :
eq_id: a = b,
Id: Id,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
equal: s = t
Definitions :
guard: {T},
implies: P 
Q,
iff: P 
Q,
rev_implies: P Q,
uimplies: b supposing a,
and: P 
Q,
member: t 
T,
eq_id: a = b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
so_lambda: 
x.t[x],
deq: EqDecider(T),
so_apply: x[s],
prop: 
Lemmas :
assert-deq,
iff_weakening_uiff,
uiff_functionality_wrt_uiff2,
id-deq_wf,
Id_wf,
equal_wf,
assert_witness,
eq_id_wf,
assert_wf,
iff_wf,
all_wf,
bool_wf,
subtype_rel_set_simple
\mforall{}[a,b:Id]. uiff(\muparrow{}a = b;a = b)
Date html generated:
2012_01_23-AM-11_53_01
Last ObjectModification:
2011_12_09-PM-07_26_10
Home
Index