---

Step * 1 of Lemma pcw-partial_wf


1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. path : Path
6. n : ℕ
⊢ <n, path> ∈ PartialPath
BY
{ (D (-2) THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
6. ∀i:ℕ. StepRel(path i;path (i + 1))
7. n : ℕ
⊢ let n,ss = <n, path> 
  in ∀i:ℕn - 1. StepRel(ss i;ss (i + 1))

---

Latex:

---

Latex:

1.  P  :  Type
2.  A  :  P  {}\mrightarrow{}  Type
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  path  :  Path
6.  n  :  \mBbbN{}
\mvdash{}  <n,  path>  \mmember{}  PartialPath


By

---

Latex:
(D  (-2)  THEN  MemTypeCD  THEN  Auto)

---

Home Index