---

{ [B,F,X,Y,es,e,v:Top].  (v  F|X, Y, Prior(self)|(e) ~ v  F|X, Y, Y|(e)) }

{ Proof }

---

Definitions occuring in Statement :  simple-comb-3: F|X, Y, Y|,  rec-combined-class-2: F|X, Y, Prior(self)|,  primed-class: Prior(X),  classrel: v  X(e),  uall: [x:A]. B[x],  top: Top,  sqequal: s ~ t
Lemmas :  top_wf

---

\mforall{}[B,F,X,Y,es,e,v:Top].    (v  \mmember{}  F|X,  Y,  Prior(self)|(e)  \msim{}  v  \mmember{}  F|X,  Y,  Y|(e))


Date html generated: 2011_08_17-PM-06_24_08
Last ObjectModification: 2011_07_23-AM-10_56_04

Home Index