---

da-agrees(da;k.T[k]) ==  k:Knd. ((k  dom(da))  T[k]  da(k))

---

Definitions :  all: x:A. B[x],  Knd: Knd,  implies: P  Q,  assert: b,  fpf-dom: x  dom(f),  ext-eq: A  B,  fpf-ap: f(x),  Kind-deq: KindDeq
FDL editor aliases :  da-agrees

---

da-agrees(da;k.T[k])  ==    \mforall{}k:Knd.  ((\muparrow{}k  \mmember{}  dom(da))  {}\mRightarrow{}  T[k]  \mequiv{}  da(k))


Date html generated: 2010_08_27-AM-12_04_07
Last ObjectModification: 2008_02_27-PM-09_50_31

Home Index