---

Step * of Lemma list-equal-set2

∀[T:Type]. ∀[P:T ⟶ ℙ].
  ∀[L:{x:T| P[x]}  List]. ∀[L':T List].  L = L' ∈ ({x:T| P[x]}  List) supposing L = L' ∈ (T List) 
  supposing ∀x:T. SqStable(P[x])
BY
{ (Auto THEN (BLemma `list-equal-set` THEN Auto) THEN BLemma `l_all-set` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}[L:\{x:T|  P[x]\}    List].  \mforall{}[L':T  List].    L  =  L'  supposing  L  =  L'  supposing  \mforall{}x:T.  SqStable(P[x])


By

---

Latex:
(Auto  THEN  (BLemma  `list-equal-set`  THEN  Auto)  THEN  BLemma  `l\_all-set`  THEN  Auto)

---

Home Index