---

Step * of Lemma rsc4_init_wf

rsc4_init()  A:'. (A  Id  bag(A))
BY
{ Try (Unfold `vatype` 0) THEN ProveWfLemma'' }

---

rsc4\_init()  \mmember{}  \mcap{}A:\mBbbU{}'.  (A  {}\mrightarrow{}  Id  {}\mrightarrow{}  bag(A))


By

---

Try  (Unfold  `vatype`  0)  THEN  ProveWfLemma''



Home Index