---

Step * of Lemma sqequal-fix-lemma1

∀[F,G,H:Base].  fix(F) fix(G) ~ fix((λx.(inl H[x]))) supposing ∀a,b:Base.  (F a (G b) ~ inl H[a b])
BY
{ (Auto
   THEN SqequalInduction
   THEN Auto
   THEN (RW UnrollLoopsOnceC 0
         THEN (RWO "-1" 0 THENA Auto)
         THEN (SqequalNCanonicalCD THEN Auto)
         THEN Unfold `so_apply` 0
         THEN SqequalNNonCanonicalCD
         THEN Auto
         THEN BackThruSomeHyp
         THEN Auto)⋅) }

---

Latex:


\mforall{}[F,G,H:Base].    fix(F)  fix(G)  \msim{}  fix((\mlambda{}x.(inl  H[x])))  supposing  \mforall{}a,b:Base.    (F  a  (G  b)  \msim{}  inl  H[a  b])


By

(Auto
  THEN  SqequalInduction
  THEN  Auto
  THEN  (RW  UnrollLoopsOnceC  0
              THEN  (RWO  "-1"  0  THENA  Auto)
              THEN  (SqequalNCanonicalCD  THEN  Auto)
              THEN  Unfold  `so\_apply`  0
              THEN  SqequalNNonCanonicalCD
              THEN  Auto
              THEN  BackThruSomeHyp
              THEN  Auto)\mcdot{})

---

Home Index