---

Step * 1 2 3 of Lemma norm-intransit_wf


1. M : Type ─→ Type
2. i3 : ℤ
3. i4 : Id
4. i5 : Id
5. i6 : pCom(P.M[P])
6. v : "choose":Id@i
7. i6 = v ∈ "choose":Id@i
⊢ (v)↓
BY
{ (D (-2) THEN RepUR ``has-value`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  i3  :  \mBbbZ{}
3.  i4  :  Id
4.  i5  :  Id
5.  i6  :  pCom(P.M[P])
6.  v  :  "choose":Id@i
7.  i6  =  v@i
\mvdash{}  (v)\mdownarrow{}


By

---

Latex:
(D  (-2)  THEN  RepUR  ``has-value``  0  THEN  Auto)

---

Home Index