---

{ [X,es,e:Top].  (X([e]) ~ [X(e)]) }

{ Proof }

---

Definitions occuring in Statement :  eclass-vals: X(L),  eclass-val: X(e),  uall: [x:A]. B[x],  top: Top,  cons: [car / cdr],  nil: [],  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  eclass-vals: X(L),  map: map(f;as),  ycomb: Y,  member: t  T
Lemmas :  top_wf

---

\mforall{}[X,es,e:Top].    (X([e])  \msim{}  [X(e)])


Date html generated: 2011_08_16-PM-04_08_48
Last ObjectModification: 2011_06_20-AM-00_42_14

Home Index