---

Step * 1 1 of Lemma sub-equality

.....set predicate..... 
1. T : Type
2. P : T ⟶ ℙ
3. i : T
4. u : T
5. i = u ∈ T
6. P u
⊢ {j:T| P j} 
BY
{ (UseWitness ⌜u⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  i  :  T
4.  u  :  T
5.  i  =  u
6.  P  u
\mvdash{}  \{j:T|  P  j\} 


By

---

Latex:
(UseWitness  \mkleeneopen{}u\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index