Step * of Lemma sqequal-list_accum

`∀[F:Base]`
`  ∀[G:Base]`
`    ∀[H,J:Base].`
`      ∀as,b1,b2:Base.`
`        F[accumulate (with value v and list item a):`
`           H[v;a]`
`          over list:`
`            as`
`          with starting value:`
`           b1)] ~ G[accumulate (with value v and list item a):`
`                     J[v;a]`
`                    over list:`
`                      as`
`                    with starting value:`
`                     b2)] `
`        supposing F[b1] ~ G[b2] `
`      supposing (∀a,r1,r2:Base.  ((F[r1] ≤ G[r2]) `` (F[H[r1;a]] ≤ G[J[r2;a]])))`
`      ∧ (∀a,r1,r2:Base.  ((G[r1] ≤ F[r2]) `` (G[J[r1;a]] ≤ F[H[r2;a]]))) `
`    supposing strict1(λx.G[x]) `
`  supposing strict1(λx.F[x])`
BY
`{ ((UnivCD THENA Auto)`
`   THEN SqequalSqle`
`   THEN SplitAndHyps`
`   THEN ((InstLemma `sqle-list_accum` [⌜F⌝;⌜G⌝;⌜H⌝;⌜J⌝;⌜as⌝;⌜b1⌝;⌜b2⌝]⋅`
`          THEN (Trivial ORELSE (HypSubst'  (-1) 0 THEN Complete (SqLeCD)))`
`          )`
`   ORELSE (InstLemma `sqle-list_accum` [⌜G⌝;⌜F⌝;⌜J⌝;⌜H⌝;⌜as⌝;⌜b2⌝;⌜b1⌝]⋅`
`           THEN (Trivial ORELSE (HypSubst'  (-1) 0 THEN Complete (SqLeCD)))`
`           )`
`   )) }`

Latex:

Latex:
\mforall{}[F:Base]
\mforall{}[G:Base]
\mforall{}[H,J:Base].
\mforall{}as,b1,b2:Base.
F[accumulate  (with  value  v  and  list  item  a):
H[v;a]
over  list:
as
with  starting  value:
b1)]  \msim{}  G[accumulate  (with  value  v  and  list  item  a):
J[v;a]
over  list:
as
with  starting  value:
b2)]
supposing  F[b1]  \msim{}  G[b2]
supposing  (\mforall{}a,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[r1;a]]  \mleq{}  G[J[r2;a]])))
\mwedge{}  (\mforall{}a,r1,r2:Base.    ((G[r1]  \mleq{}  F[r2])  {}\mRightarrow{}  (G[J[r1;a]]  \mleq{}  F[H[r2;a]])))
supposing  strict1(\mlambda{}x.G[x])
supposing  strict1(\mlambda{}x.F[x])

By

Latex:
((UnivCD  THENA  Auto)
THEN  SqequalSqle
THEN  SplitAndHyps
THEN  ((InstLemma  `sqle-list\_accum`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}
THEN  (Trivial  ORELSE  (HypSubst'    (-1)  0  THEN  Complete  (SqLeCD)))
)
ORELSE  (InstLemma  `sqle-list\_accum`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}
THEN  (Trivial  ORELSE  (HypSubst'    (-1)  0  THEN  Complete  (SqLeCD)))
)
))

Home Index