Step * 1 of Lemma l_subset_append2


1. [T] Type
2. L1 List
3. L2 List
4. L1' List
5. L2' List
6. l_subset(T;L1;L1')
7. l_subset(T;L2;L2')
⊢ l_subset(T;L1;L1' L2')
BY
(RepeatFor (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')
\mvdash{}  l\_subset(T;L1;L1'  @  L2')


By


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




Home Index