---

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

{ Proof }

---

Definitions occuring in Statement :  name_eq: name_eq(x;y),  name: Name,  uall: [x:A]. B[x],  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  member: t  T,  implies: P  Q,  prop: ,  iff: P  Q,  and: P  Q,  rev_implies: P  Q,  sq_type: SQType(T),  uimplies: b supposing a,  all: x:A. B[x],  guard: {T}
Lemmas :  subtype_base_sq,  bool_wf,  bool_subtype_base,  name_wf,  name_eq_wf,  assert_wf,  iff_imp_equal_bool,  iff_functionality_wrt_iff,  iff_weakening_uiff,  assert-name_eq

---

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


Date html generated: 2011_08_10-AM-07_42_20
Last ObjectModification: 2011_06_18-AM-08_09_35

Home Index