---

Step * of Lemma list_accum_equality

∀[T,A,B,C:Type]. ∀[f:A ⟶ T ⟶ A]. ∀[g:B ⟶ T ⟶ B]. ∀[F:A ⟶ C]. ∀[G:B ⟶ C].
  ∀[L:T List]. ∀[a0:A]. ∀[b0:B].
    F[accumulate (with value a and list item x):
       f[a;x]
      over list:
        L
      with starting value:
       a0)]
    = G[accumulate (with value b and list item x):
         g[b;x]
        over list:
          L
        with starting value:
         b0)]
    ∈ C 
    supposing F[a0] = G[b0] ∈ C 
  supposing ∀a:A. ∀b:B. ∀x:T.  (((F a) = (G b) ∈ C) ⇒ (F[f[a;x]] = G[g[b;x]] ∈ C))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN RepeatFor 2 (BackThruSomeHyp) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A].  \mforall{}[g:B  {}\mrightarrow{}  T  {}\mrightarrow{}  B].  \mforall{}[F:A  {}\mrightarrow{}  C].  \mforall{}[G:B  {}\mrightarrow{}  C].
    \mforall{}[L:T  List].  \mforall{}[a0:A].  \mforall{}[b0:B].
        F[accumulate  (with  value  a  and  list  item  x):
              f[a;x]
            over  list:
                L
            with  starting  value:
              a0)]
        =  G[accumulate  (with  value  b  and  list  item  x):
                  g[b;x]
                over  list:
                    L
                with  starting  value:
                  b0)] 
        supposing  F[a0]  =  G[b0] 
    supposing  \mforall{}a:A.  \mforall{}b:B.  \mforall{}x:T.    (((F  a)  =  (G  b))  {}\mRightarrow{}  (F[f[a;x]]  =  G[g[b;x]]))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  RepeatFor  2  (BackThruSomeHyp)  THEN  Auto)

---

Home Index