---

Step * of Lemma fset-null_wf

∀[T:Type]. ∀[s:fset(T)].  (fset-null(s) ∈ 𝔹)
BY
{ (Auto THEN (D -1 THEN Auto) THEN Unfold `fset-null` 0 THEN Auto) }

1
1. T : Type
2. s : Base
3. s1 : Base
4. s = s1 ∈ pertype(λx,y. ((x ∈ T List) ∧ (y ∈ T List) ∧ set-equal(T;x;y)))
5. s ∈ T List
6. s1 ∈ T List
7. set-equal(T;s;s1)
⊢ null(s) = null(s1)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s:fset(T)].    (fset-null(s)  \mmember{}  \mBbbB{})


By

---

Latex:
(Auto  THEN  (D  -1  THEN  Auto)  THEN  Unfold  `fset-null`  0  THEN  Auto)

---

Home Index