Step * 1 1 of Lemma UallTest1

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


Latex:


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


By

Auto




Home Index