---

{ [x,y:Name].  (name_eq(x;y)  ) }

{ Proof }

---

Definitions occuring in Statement :  name_eq: name_eq(x;y),  name: Name,  bool: ,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  name_eq: name_eq(x;y),  deq: EqDecider(T),  all: x:A. B[x],  iff: P  Q,  prop: ,  and: P  Q,  implies: P  Q,  rev_implies: P  Q
Lemmas :  name_wf,  name-deq_wf,  bool_wf,  iff_wf,  assert_wf

---

\mforall{}[x,y:Name].    (name\_eq(x;y)  \mmember{}  \mBbbB{})


Date html generated: 2011_08_10-AM-07_42_15
Last ObjectModification: 2011_06_18-AM-08_09_26

Home Index