---

Step * 1 of Lemma accessible-iff


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [t] : T
4. pW t@i
⊢ ∀u:T. (R[u;t] ⇒ (pW u))
BY
{ pWD (-1)⋅ }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [t] : T
4. a : Unit
5. b:(x:T × R[x;t]) ⟶ (pW (fst(b)))
⊢ ∀u:T. (R[u;t] ⇒ (pW u))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  [t]  :  T
4.  pW  t@i
\mvdash{}  \mforall{}u:T.  (R[u;t]  {}\mRightarrow{}  (pW  u))


By

---

Latex:
pWD  (-1)\mcdot{}

---

Home Index