---

Step * 1 2 of Lemma norm-intransit_wf

.....aux..... 
1. M : Type ─→ Type
2. i3 : ℤ
3. i4 : Id
4. i5 : Id
5. i6 : pCom(P.M[P])
⊢ (i6)↓
BY
{ GenConclAtAddrType ⌈"choose":Id⌉ [1]⋅ }

1
.....wf..... 
1. M : Type ─→ Type
2. i3 : ℤ
3. i4 : Id
4. i5 : Id
5. i6 : pCom(P.M[P])
⊢ i6 ∈ "choose":Id

2
.....wf..... 
1. M : Type ─→ Type
2. i3 : ℤ
3. i4 : Id
4. i5 : Id
5. i6 : pCom(P.M[P])
⊢ "choose":Id ∈ Type

3
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)↓

---

Latex:

---

Latex:
.....aux..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  i3  :  \mBbbZ{}
3.  i4  :  Id
4.  i5  :  Id
5.  i6  :  pCom(P.M[P])
\mvdash{}  (i6)\mdownarrow{}


By

---

Latex:
GenConclAtAddrType  \mkleeneopen{}"choose":Id\mkleeneclose{}  [1]\mcdot{}

---

Home Index