---

Step * of Lemma l_subset_cons

∀[T:Type]. ∀x:T. ∀L1:T List.  ∀[L2:T List]. (l_subset(T;[x / L1];L2) ⇐⇒ (x ∈ L2) ∧ l_subset(T;L1;L2))
BY
{ (Auto
   THEN All (Unfold `l_subset`)
   THEN Auto
   THEN Try (Complete ((GenListD (-1) THEN D (-1) THEN Auto)))
   THEN OnSomeHyp (\i. BHyp i)
   THEN Auto
   THEN GenListD 0
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}x:T.  \mforall{}L1:T  List.    \mforall{}[L2:T  List].  (l\_subset(T;[x  /  L1];L2)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L2)  \mwedge{}  l\_subset(T;L1;L2))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `l\_subset`)
  THEN  Auto
  THEN  Try  (Complete  ((GenListD  (-1)  THEN  D  (-1)  THEN  Auto)))
  THEN  OnSomeHyp  (\mbackslash{}i.  BHyp  i)
  THEN  Auto
  THEN  GenListD  0
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto))))

---

Home Index