---

Step * 1 1 of Lemma fset-null_wf


1. T : Type
2. v : T List
3. v1 : T List
4. set-equal(T;v1;v)
⊢ null(v1) = null(v)
BY
{ (D -2
   THEN D 2
   THEN Reduce 0
   THEN Auto
   THEN UnfoldTopAb (-1)
   THEN InstHyp [⌜u⌝] (-1)⋅
   THEN Auto
   THEN OnMaybeHyp 5 (\h. (D h THEN Complete (Auto)))) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  v  :  T  List
3.  v1  :  T  List
4.  set-equal(T;v1;v)
\mvdash{}  null(v1)  =  null(v)


By

---

Latex:
(D  -2
  THEN  D  2
  THEN  Reduce  0
  THEN  Auto
  THEN  UnfoldTopAb  (-1)
  THEN  InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  OnMaybeHyp  5  (\mbackslash{}h.  (D  h  THEN  Complete  (Auto))))

---

Home Index