---

Step * 1 1 of Lemma accessible-iff


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))
BY
{ (RenameVar `f' (-1) THEN Auto) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `f'  (-1)  THEN  Auto)

---

Home Index