---

Step * 1 of Lemma UallTest1


1. F : ∀[T:Type]. (T ─→ T)@i'
2. S : Type@i'
3. s : S@i
⊢ (F s) = s ∈ S
BY
{ Assert ⌈∀x:{y:S| y = s ∈ S} . (F x ∈ {y:S| y = s ∈ S} )⌉⋅ }

1
.....assertion..... 
1. F : ∀[T:Type]. (T ─→ T)@i'
2. S : Type@i'
3. s : S@i
⊢ ∀x:{y:S| y = s ∈ S} . (F x ∈ {y:S| y = s ∈ S} )

2
1. F : ∀[T:Type]. (T ─→ T)@i'
2. S : Type@i'
3. s : S@i
4. ∀x:{y:S| y = s ∈ S} . (F x ∈ {y:S| y = s ∈ S} )
⊢ (F s) = s ∈ S

---

Latex:



1.  F  :  \mforall{}[T:Type].  (T  {}\mrightarrow{}  T)@i'
2.  S  :  Type@i'
3.  s  :  S@i
\mvdash{}  (F  s)  =  s


By

Assert  \mkleeneopen{}\mforall{}x:\{y:S|  y  =  s\}  .  (F  x  \mmember{}  \{y:S|  y  =  s\}  )\mkleeneclose{}\mcdot{}

---

Home Index