---

Step * 1 of Lemma processComm_wf2


1. cSt : Type
⊢ "msg"×PiDataVal() ⊆r "msg":PiDataVal() |+ "create":cSt |+ "choose":Id |+ "new":Unit
BY
{ RepeatFor 3 ((BLemma_o (ioid Obid: subtype_rel_tagged+_general)⋅
                THEN Auto
                THEN Try ((BLemma `tag-by-subtype-tag-case`⋅ THEN Reduce 0 THEN Auto)))) }

---

Latex:

---

Latex:

1.  cSt  :  Type
\mvdash{}  "msg"\mtimes{}PiDataVal()  \msubseteq{}r  "msg":PiDataVal()  |+  "create":cSt  |+  "choose":Id  |+  "new":Unit


By

---

Latex:
RepeatFor  3  ((BLemma\_o  (ioid  Obid:  subtype\_rel\_tagged+\_general)\mcdot{}
                            THEN  Auto
                            THEN  Try  ((BLemma  `tag-by-subtype-tag-case`\mcdot{}  THEN  Reduce  0  THEN  Auto))))

---

Home Index