---

Step * 1 1 1 2 of Lemma fset-item_wf


1. T : Type
2. v : T List
3. u : T
4. v2 : T List
5. set-equal(T;v;[u / v2])
6. 1 ≤ ||v||
⊢ (||v2|| + 1) ≥ 1 
BY
{ ((Assert 0 ≤ ||v2|| BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  v  :  T  List
3.  u  :  T
4.  v2  :  T  List
5.  set-equal(T;v;[u  /  v2])
6.  1  \mleq{}  ||v||
\mvdash{}  (||v2||  +  1)  \mgeq{}  1 


By

---

Latex:
((Assert  0  \mleq{}  ||v2||  BY  Auto)  THEN  Auto)

---

Home Index