---

Step * of Lemma UallTest1

∀F:∀[T:Type]. (T ─→ T). ∀S:Type. ∀s:S.  ((F s) = s ∈ S)
BY
{ Auto }

1
1. F : ∀[T:Type]. (T ─→ T)@i'
2. S : Type@i'
3. s : S@i
⊢ (F s) = s ∈ S

---

Latex:


\mforall{}F:\mforall{}[T:Type].  (T  {}\mrightarrow{}  T).  \mforall{}S:Type.  \mforall{}s:S.    ((F  s)  =  s)


By

Auto

---

Home Index