---

Step * of Lemma l_subset_append

∀[T:Type]. ∀[L:T List].  ∀L1,L2:T List.  (l_subset(T;L1 @ L2;L) ⇐⇒ l_subset(T;L1;L) ∧ l_subset(T;L2;L))
BY
{ (Auto
   THEN All (Unfold `l_subset`)
   THEN Auto
   THEN Try (Complete ((BackThruSomeHyp THEN GenListD 0 THEN Auto)))
   THEN SimpleReasoningSteps) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  All  (Unfold  `l\_subset`)
  THEN  Auto
  THEN  Try  (Complete  ((BackThruSomeHyp  THEN  GenListD  0  THEN  Auto)))
  THEN  SimpleReasoningSteps)

---

Home Index