---

Step * 2 of Lemma concat-is-nil


1. T : Type
2. u : T List
3. v : T List List
4. uiff(concat(v) = [] ∈ (T List);(∀L∈v.L = [] ∈ (T List)))
⊢ uiff((u @ concat(v)) = [] ∈ (T List);(u = [] ∈ (T List)) ∧ (∀L∈v.L = [] ∈ (T List)))
BY
{ (RWO "append_is_nil" 0 THEN Auto THEN BackThruSomeHyp THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T  List
3.  v  :  T  List  List
4.  uiff(concat(v)  =  [];(\mforall{}L\mmember{}v.L  =  []))
\mvdash{}  uiff((u  @  concat(v))  =  [];(u  =  [])  \mwedge{}  (\mforall{}L\mmember{}v.L  =  []))


By

---

Latex:
(RWO  "append\_is\_nil"  0  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)\mcdot{}

---

Home Index