---

Step * 1 of Lemma com-kind_wf


1. M : Type ─→ Type
2. c : pCom(P.M[P])
⊢ c.tag ∈ Atom
BY
{ (RepUR ``pCom Com`` -1 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  c  :  pCom(P.M[P])
\mvdash{}  c.tag  \mmember{}  Atom


By

---

Latex:
(RepUR  ``pCom  Com``  -1  THEN  Auto)\mcdot{}

---

Home Index