---

Step * of Lemma member_list_accum_l_subset2

∀[T:Type]
  ∀f:(T List) ⟶ T ⟶ (T List). ∀L,a:T List. ∀x:T.
    ((∀a:T List. ∀x:T.  l_subset(T;f[a;x];[x / a]))
    ⇒ (x ∈ accumulate (with value a and list item x):
             f[a;x]
            over list:
              L
            with starting value:
             a))
    ⇒ ((x ∈ a) ∨ (x ∈ L)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN (FHyp (-5) [-1] THENA Auto)
   THEN D (-1)
   THEN Try (Complete (((OrRight THENA Auto) THEN GenListD 0⋅ THEN OrRight THEN Auto)))
   THEN Unfold `l_subset` (-3)
   THEN (FHyp (-3) [-1] THENA Auto)
   THEN GenListD (-1)⋅
   THEN D (-1)
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN (OrRight THENA Auto)
   THEN GenListD 0
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:(T  List)  {}\mrightarrow{}  T  {}\mrightarrow{}  (T  List).  \mforall{}L,a:T  List.  \mforall{}x:T.
        ((\mforall{}a:T  List.  \mforall{}x:T.    l\_subset(T;f[a;x];[x  /  a]))
        {}\mRightarrow{}  (x  \mmember{}  accumulate  (with  value  a  and  list  item  x):
                          f[a;x]
                        over  list:
                            L
                        with  starting  value:
                          a))
        {}\mRightarrow{}  ((x  \mmember{}  a)  \mvee{}  (x  \mmember{}  L)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  (FHyp  (-5)  [-1]  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  (((OrRight  THENA  Auto)  THEN  GenListD  0\mcdot{}  THEN  OrRight  THEN  Auto)))
  THEN  Unfold  `l\_subset`  (-3)
  THEN  (FHyp  (-3)  [-1]  THENA  Auto)
  THEN  GenListD  (-1)\mcdot{}
  THEN  D  (-1)
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  (OrRight  THENA  Auto)
  THEN  GenListD  0
  THEN  OrLeft
  THEN  Auto)

---

Home Index