{ locknd-deq() 
EqDecider(LocKnd) }
{ Proof }
Definitions occuring in Statement :
locknd-deq: locknd-deq(),
LocKnd: LocKnd,
member: t T,
deq: EqDecider(T)
Definitions :
member: t T,
LocKnd: LocKnd,
locknd-deq: locknd-deq(),
prop: 
,
so_lambda: 
x.t[x],
all: 
x:A. B[x],
implies: P 
Q,
so_apply: x[s]
Lemmas :
product-deq_wf,
Id_wf,
Knd_wf,
id-deq_wf,
Kind-deq_wf,
strong-subtype-deq-subtype,
assert_wf,
hasloc_wf,
strong-subtype-set3,
strong-subtype-self
locknd-deq() \mmember{} EqDecider(LocKnd)
Date html generated:
2010_08_26-PM-11_42_19
Last ObjectModification:
2008_02_27-PM-09_35_00
Home
Index