---

Step * 2 of Lemma accessible-iff


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [t] : T
4. ∀u:T. (R[u;t] ⇒ (pW u))@i
⊢ pW t
BY
{ (RenameVar `f' (-1) THEN (UseWitness ⌜<⋅, λp.(f (fst(p)) (snd(p)))>⌝⋅ THEN  pWD 0⋅) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `f'  (-1)  THEN  (UseWitness  \mkleeneopen{}<\mcdot{},  \mlambda{}p.(f  (fst(p))  (snd(p)))>\mkleeneclose{}\mcdot{}  THEN    pWD  0\mcdot{})  THEN  Auto)

---

Home Index