{ 
[x,y:Name]. uiff(
name_eq(x;y);x = y) }
{ Proof }
Definitions occuring in Statement :
name_eq: name_eq(x;y),
name: Name,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
equal: s = t
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
name_eq: name_eq(x;y),
member: t 
T,
and: P 
Q,
uimplies: b supposing a,
prop: 
,
deq: EqDecider(T),
all: x:A. B[x],
iff: P 
Q,
implies: P Q,
rev_implies: P Q,
eqof: eqof(d)
Lemmas :
assert_wf,
assert_witness,
name_wf,
deq_property,
name-deq_wf,
bool_wf,
iff_wf
\mforall{}[x,y:Name]. uiff(\muparrow{}name\_eq(x;y);x = y)
Date html generated:
2011_08_10-AM-07_42_17
Last ObjectModification:
2011_06_18-AM-08_09_34
Home
Index