---

Step * of Lemma concat-is-nil

∀[T:Type]. ∀[LL:T List List].  uiff(concat(LL) = [] ∈ (T List);(∀L∈LL.L = [] ∈ (T List)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN ((RWW "l_all_cons" 0 THENA Auto) THEN Try ((Unfold `concat` 0 THEN Reduce 0 THEN Fold `concat` 0)))⋅) }

1
1. T : Type
⊢ uiff([] = [] ∈ (T List);(∀L∈[].L = [] ∈ (T List)))

2
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)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[LL:T  List  List].    uiff(concat(LL)  =  [];(\mforall{}L\mmember{}LL.L  =  []))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  ((RWW  "l\_all\_cons"  0  THENA  Auto)
              THEN  Try  ((Unfold  `concat`  0  THEN  Reduce  0  THEN  Fold  `concat`  0))
              )\mcdot{})

---

Home Index