---

{ f,g:x:Knd fp-> Type. x:Knd.
    (x  dom(f  g)  (x  dom(f))  (x  dom(g))) }

{ Proof }

---

Definitions occuring in Statement :  fpf-join: f  g,  fpf-dom: x  dom(f),  fpf: a:A fp-> B[a],  Kind-deq: KindDeq,  Knd: Knd,  assert: b,  all: x:A. B[x],  iff: P  Q,  or: P  Q,  universe: Type
Definitions :  member: t  T,  so_lambda: x.t[x],  all: x:A. B[x],  rev_implies: P  Q,  iff: P  Q,  implies: P  Q,  prop: ,  and: P  Q,  or: P  Q,  so_apply: x[s]
Lemmas :  fpf_wf,  Knd_wf,  fpf-dom_wf,  fpf-join_wf,  assert_wf,  Kind-deq_wf,  top_wf,  fpf-trivial-subtype-top,  fpf-join-dom,  iff_functionality_wrt_iff

---

\mforall{}f,g:x:Knd  fp->  Type.  \mforall{}x:Knd.    (\muparrow{}x  \mmember{}  dom(f  \moplus{}  g)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))  \mvee{}  (\muparrow{}x  \mmember{}  dom(g)))


Date html generated: 2010_08_27-AM-12_00_18
Last ObjectModification: 2008_02_27-PM-09_46_01

Home Index