---

Step * of Lemma equiv-on-corec

∀F:Type ⟶ Type
  (ContinuousMonotone(T.F[T])
  ⇒ (∀G:⋂T:Type. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
        ((∀T:Type. ∀E:T ⟶ T ⟶ ℙ.  (EquivRel(T;x,y.E x y) ⇒ EquivRel(F[T];x,y.G E x y)))
        ⇒ EquivRel(corec(T.F[T]);x,y.corec-rel(G) x y))))
BY
{ ((Auto
    THEN (Assert ∀n:ℕ. (G^n (λx,y. True) ∈ primrec(n;Top;λ,T. F[T]) ⟶ primrec(n;Top;λ,T. F[T]) ⟶ ℙ) BY
                (InductionOnNat
                 THEN (RWO "fun_exp_unroll" 0 THENA Auto)
                 THEN (RWO "primrec-unroll" 0 THENA Auto)
                 THEN Reduce 0
                 THEN Try ((((Subst' (n =z 0) ~ ff 0 THENA Complete (Auto))
                             THEN (Subst' n <z 1 ~ ff 0 THENA Complete (Auto))
                             )
                            THEN Reduce 0
                            THEN Auto))
                 THEN Auto))
    )
   THEN (Assert ∀n:ℕ. EquivRel(primrec(n;Top;λ,T. F[T]);x,y.G^n (λx,y. True) x y) BY
               ((InductionOnNat
                 THENW (Auto THEN ((InstHyp [⌜n1⌝] 5⋅ THEN Auto) ORELSE (InstHyp [⌜n - 1⌝] 5⋅ THEN Auto)))
                 )
                THEN (RWO "fun_exp_unroll" 0 THENA Auto)
                THEN (RWO "primrec-unroll" 0 THENA Auto)
                THEN Reduce 0
                THEN Try ((((Subst' (n =z 0) ~ ff 0 THENA Complete (Auto))
                            THEN (Subst' n <z 1 ~ ff 0 THENA Complete (Auto))
                            )
                           THEN Reduce 0
                           THEN Auto))
                THEN Auto))
   ) }

1
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. G : ⋂T:Type. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
4. ∀T:Type. ∀E:T ⟶ T ⟶ ℙ.  (EquivRel(T;x,y.E x y) ⇒ EquivRel(F[T];x,y.G E x y))
5. ∀n:ℕ. (G^n (λx,y. True) ∈ primrec(n;Top;λ,T. F[T]) ⟶ primrec(n;Top;λ,T. F[T]) ⟶ ℙ)
6. ∀n:ℕ. EquivRel(primrec(n;Top;λ,T. F[T]);x,y.G^n (λx,y. True) x y)
⊢ EquivRel(corec(T.F[T]);x,y.corec-rel(G) x y)

---

Latex:

---

Latex:
\mforall{}F:Type  {}\mrightarrow{}  Type
    (ContinuousMonotone(T.F[T])
    {}\mRightarrow{}  (\mforall{}G:\mcap{}T:Type.  ((T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  \mBbbP{})
                ((\mforall{}T:Type.  \mforall{}E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.    (EquivRel(T;x,y.E  x  y)  {}\mRightarrow{}  EquivRel(F[T];x,y.G  E  x  y)))
                {}\mRightarrow{}  EquivRel(corec(T.F[T]);x,y.corec-rel(G)  x  y))))


By

---

Latex:
((Auto
    THEN  (Assert  \mforall{}n:\mBbbN{}.  (G\^{}n  (\mlambda{}x,y.  True)  \mmember{}  primrec(n;Top;\mlambda{},T.  F[T])  {}\mrightarrow{}  primrec(n;Top;\mlambda{},T.  F[T])  {}\mrightarrow{}  \mBbbP{})  \000CBY
                            (InductionOnNat
                              THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
                              THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                              THEN  Reduce  0
                              THEN  Try  ((((Subst'  (n  =\msubz{}  0)  \msim{}  ff  0  THENA  Complete  (Auto))
                                                      THEN  (Subst'  n  <z  1  \msim{}  ff  0  THENA  Complete  (Auto))
                                                      )
                                                    THEN  Reduce  0
                                                    THEN  Auto))
                              THEN  Auto))
    )
  THEN  (Assert  \mforall{}n:\mBbbN{}.  EquivRel(primrec(n;Top;\mlambda{},T.  F[T]);x,y.G\^{}n  (\mlambda{}x,y.  True)  x  y)  BY
                          ((InductionOnNat
                              THENW  (Auto
                                            THEN  ((InstHyp  [\mkleeneopen{}n1\mkleeneclose{}]  5\mcdot{}  THEN  Auto)  ORELSE  (InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  5\mcdot{}  THEN  Auto))
                                            )
                              )
                            THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
                            THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  Try  ((((Subst'  (n  =\msubz{}  0)  \msim{}  ff  0  THENA  Complete  (Auto))
                                                    THEN  (Subst'  n  <z  1  \msim{}  ff  0  THENA  Complete  (Auto))
                                                    )
                                                  THEN  Reduce  0
                                                  THEN  Auto))
                            THEN  Auto))
  )

---

Home Index