---

Step * 1 of Lemma fset-null_wf


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)
BY
{ (MoveToConcl (-1) THEN GenConclTerms Auto [⌜s1⌝;⌜s⌝]⋅ THEN All Thin THEN Auto) }

1
1. T : Type
2. v : T List
3. v1 : T List
4. set-equal(T;v1;v)
⊢ null(v1) = null(v)

---

Latex:

---

Latex:

1.  T  :  Type
2.  s  :  Base
3.  s1  :  Base
4.  s  =  s1
5.  s  \mmember{}  T  List
6.  s1  \mmember{}  T  List
7.  set-equal(T;s;s1)
\mvdash{}  null(s)  =  null(s1)


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclTerms  Auto  [\mkleeneopen{}s1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THEN  All  Thin  THEN  Auto)

---

Home Index