---

Step * 2 of Lemma l_subset_append2


1. [T] : Type
2. L1 : T List
3. L2 : T List
4. L1' : T List
5. L2' : T List
6. l_subset(T;L1;L1')
7. l_subset(T;L2;L2')
8. l_subset(T;L1;L1' @ L2')
⊢ l_subset(T;L2;L1' @ L2')
BY
{ (RepeatFor 2 (ParallelOp -2) THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  L1'  :  T  List
5.  L2'  :  T  List
6.  l\_subset(T;L1;L1')
7.  l\_subset(T;L2;L2')
8.  l\_subset(T;L1;L1'  @  L2')
\mvdash{}  l\_subset(T;L2;L1'  @  L2')


By

---

Latex:
(RepeatFor  2  (ParallelOp  -2)  THEN  ParallelLast  THEN  Auto)

---

Home Index