---

Step * of Lemma list-eq-set-type

∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[A,B:T List].
  (A = B ∈ ({x:T| P[x]}  List)) supposing ((∀i:ℕ||A||. P[A[i]]) and (A = B ∈ (T List)))
BY
{ (Auto THEN BLemma `list-set-type2` THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:T  List].    (A  =  B)  supposing  ((\mforall{}i:\mBbbN{}||A||.  P[A[i]])  and  (A  =  B))


By

---

Latex:
(Auto  THEN  BLemma  `list-set-type2`  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index