---

Step * 1 1 1 of Lemma accessible-iff


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [t] : T
4. a : Unit
5. f : b:(x:T × R[x;t]) ⟶ (pW (fst(b)))
6. u : T@i
7. R[u;t]@i
⊢ pW u
BY
{ (RenameVar `z' (-1) THEN UseWitness ⌜f <u, z>⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  [t]  :  T
4.  a  :  Unit
5.  f  :  b:(x:T  \mtimes{}  R[x;t])  {}\mrightarrow{}  (pW  (fst(b)))
6.  u  :  T@i
7.  R[u;t]@i
\mvdash{}  pW  u


By

---

Latex:
(RenameVar  `z'  (-1)  THEN  UseWitness  \mkleeneopen{}f  <u,  z>\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index