---

Step * 1 of Lemma l_all_single


1. [T] : Type
2. t : T
3. [P] : {x:T| x = t ∈ T}  ⟶ ℙ
4. ∀i:ℕ1. P[[t][i]]
⊢ P[t]
BY
{ (With ⌜0⌝  (D (-1))⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  t  :  T
3.  [P]  :  \{x:T|  x  =  t\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}i:\mBbbN{}1.  P[[t][i]]
\mvdash{}  P[t]


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}    (D  (-1))\mcdot{}  THEN  Auto)

---

Home Index