---

{ [l:IdLnk]. [k:Knd]. [tg:Id]. [v:Top].
    (k  dom(lnk-decl(l;tg : v)) ~ rcv(l,tg) = k) }

{ Proof }

---

Definitions occuring in Statement :  lnk-decl: lnk-decl(l;dt),  fpf-single: x : v,  fpf-dom: x  dom(f),  eq_knd: a = b,  Kind-deq: KindDeq,  rcv: rcv(l,tg),  Knd: Knd,  IdLnk: IdLnk,  Id: Id,  uall: [x:A]. B[x],  top: Top,  sqequal: s ~ t
Definitions :  fpf-dom: x  dom(f),  lnk-decl: lnk-decl(l;dt),  fpf-single: x : v,  deq-member: deq-member(eq;x;L),  pi1: fst(t),  map: map(f;as),  ycomb: Y,  reduce: reduce(f;k;as),  bor: p q,  bfalse: ff,  member: t  T,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  prop: ,  ifthenelse: if b then t else f fi ,  bool: ,  uall: [x:A]. B[x],  unit: Unit,  iff: P  Q,  and: P  Q,  eq_knd: a = b,  it:
Lemmas :  eq_knd_wf,  rcv_wf,  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  top_wf,  Id_wf,  Knd_wf,  IdLnk_wf

---

\mforall{}[l:IdLnk].  \mforall{}[k:Knd].  \mforall{}[tg:Id].  \mforall{}[v:Top].    (k  \mmember{}  dom(lnk-decl(l;tg  :  v))  \msim{}  rcv(l,tg)  =  k)


Date html generated: 2011_08_10-AM-08_10_21
Last ObjectModification: 2011_06_18-AM-08_26_21

Home Index