---

Step * of Lemma l_subset_append2

∀[T:Type]. ∀L1,L2,L1',L2':T List.  ((l_subset(T;L1;L1') ∧ l_subset(T;L2;L2')) ⇒ l_subset(T;L1 @ L2;L1' @ L2'))
BY
{ (Auto THEN BLemma `l_subset_append` THEN Auto) }

1
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')
⊢ l_subset(T;L1;L1' @ L2')

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

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L1,L2,L1',L2':T  List.
        ((l\_subset(T;L1;L1')  \mwedge{}  l\_subset(T;L2;L2'))  {}\mRightarrow{}  l\_subset(T;L1  @  L2;L1'  @  L2'))


By

---

Latex:
(Auto  THEN  BLemma  `l\_subset\_append`  THEN  Auto)

---

Home Index