---

Step * 1 of Lemma assert-fset-null


1. T : Type
2. s : fset(T)
3. ↑fset-null(s)
⊢ s = {} ∈ fset(T)
BY
{ (newQuotD 2 THEN All (RepUR ``fset-null empty-fset``)  THEN (RW assert_pushdownC (-1) THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  s  :  fset(T)
3.  \muparrow{}fset-null(s)
\mvdash{}  s  =  \{\}


By

---

Latex:
(newQuotD  2  THEN  All  (RepUR  ``fset-null  empty-fset``)    THEN  (RW  assert\_pushdownC  (-1)  THEN  Auto)\mcdot{})

---

Home Index