---

Step * of Lemma sqequal-list_ind

∀[F:Base]
  ∀[G:Base]
    ∀[H,J:Base].
      ∀as,b1,b2:Base.
        F[rec-case(as) of
          [] => b1
          h::t =>
           r.H[h;t;r]] ~ G[rec-case(as) of
                           [] => b2
                           h::t =>
                            r.J[h;t;r]] 
        supposing F[b1] ~ G[b2] 
      supposing (∀x,y,r1,r2:Base.  ((F[r1] ≤ G[r2]) ⇒ (F[H[x;y;r1]] ≤ G[J[x;y;r2]])))
      ∧ (∀x,y,r1,r2:Base.  ((G[r1] ≤ F[r2]) ⇒ (G[J[x;y;r1]] ≤ F[H[x;y;r2]]))) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])
BY
{ ((UnivCD THENA Auto)
   THEN SqequalSqle
   THEN SplitAndHyps
   THEN ((InstLemma `sqle-list_ind` [⌜F⌝;⌜G⌝;⌜H⌝;⌜J⌝;⌜as⌝;⌜b1⌝;⌜b2⌝]⋅
          THEN (Trivial ORELSE (HypSubst'  (-1) 0 THEN Complete (SqLeCD)))
          )
   ORELSE (InstLemma `sqle-list_ind` [⌜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[rec-case(as)  of
                    []  =>  b1
                    h::t  =>
                      r.H[h;t;r]]  \msim{}  G[rec-case(as)  of
                                                      []  =>  b2
                                                      h::t  =>
                                                        r.J[h;t;r]] 
                supposing  F[b1]  \msim{}  G[b2] 
            supposing  (\mforall{}x,y,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[x;y;r1]]  \mleq{}  G[J[x;y;r2]])))
            \mwedge{}  (\mforall{}x,y,r1,r2:Base.    ((G[r1]  \mleq{}  F[r2])  {}\mRightarrow{}  (G[J[x;y;r1]]  \mleq{}  F[H[x;y;r2]]))) 
        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\_ind`  [\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\_ind`  [\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