---

Step * of Lemma coinduction-principle

∀[F:Type ⟶ Type]
  ∀[R:corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ]
    ∀[x,y:corec(T.F[T])].  x = y ∈ corec(T.F[T]) supposing R[x;y] supposing x,y.R[x;y] is an T.F[T]-bisimulation 
  supposing ContinuousMonotone(T.F[T])
BY
{ TACTIC:RepeatFor 4 ((D 0 THENA Auto)) }

1
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. R : corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ
4. x,y.R[x;y] is an T.F[T]-bisimulation
⊢ ∀[x,y:corec(T.F[T])].  x = y ∈ corec(T.F[T]) supposing R[x;y]

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    \mforall{}[R:corec(T.F[T])  {}\mrightarrow{}  corec(T.F[T])  {}\mrightarrow{}  \mBbbP{}]
        \mforall{}[x,y:corec(T.F[T])].    x  =  y  supposing  R[x;y]  supposing  x,y.R[x;y]  is  an  T.F[T]-bisimulation 
    supposing  ContinuousMonotone(T.F[T])


By

---

Latex:
TACTIC:RepeatFor  4  ((D  0  THENA  Auto))

---

Home Index