---

Step * 2 1 of Lemma star-append-iff


1. T : Type
2. P : (T List) ⟶ ℙ
3. Q : (T List) ⟶ ℙ
4. L : T List
5. L1 : T List
6. L2 : T List
7. L = (L1 @ L2) ∈ (T List)
8. P L1
9. LL : T List List
10. L' : T List
11. (∀X∈LL.P X)
12. Q L'
13. L2 = (concat(LL) @ L') ∈ (T List)
14. (∀X∈[L1 / LL].P X)
15. Q L'
⊢ L = (concat([L1 / LL]) @ L') ∈ (T List)
BY
{ (Unfold `concat` 0
   THEN Reduce 0
   THEN Fold `concat` 0
   THEN RWO "append_assoc" 0
   THEN Auto
   THEN (RevHypSubst (-1) 0)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  Q  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
4.  L  :  T  List
5.  L1  :  T  List
6.  L2  :  T  List
7.  L  =  (L1  @  L2)
8.  P  L1
9.  LL  :  T  List  List
10.  L'  :  T  List
11.  (\mforall{}X\mmember{}LL.P  X)
12.  Q  L'
13.  L2  =  (concat(LL)  @  L')
14.  (\mforall{}X\mmember{}[L1  /  LL].P  X)
15.  Q  L'
\mvdash{}  L  =  (concat([L1  /  LL])  @  L')


By

---

Latex:
(Unfold  `concat`  0
  THEN  Reduce  0
  THEN  Fold  `concat`  0
  THEN  RWO  "append\_assoc"  0
  THEN  Auto
  THEN  (RevHypSubst  (-1)  0)
  THEN  Auto)\mcdot{}

---

Home Index