---

Step * 1 2 1 1 of Lemma coSet-equality


1. corec(T.a:Type × (a ⟶ T)) ∈ 𝕌'
2. ∀[R:corec(T.a:Type × (a ⟶ T)) ⟶ corec(T.a:Type × (a ⟶ T)) ⟶ ℙ']
     ∀[x,y:corec(T.a:Type × (a ⟶ T))].  x = y ∈ corec(T.a:Type × (a ⟶ T)) supposing R[x;y] 
     supposing F-bisimulation{i':l}(T.a:Type × (a ⟶ T); x,y.R[x;y])
3. x : coSet{i:l}
4. y : coSet{i:l}
5. R : coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
6. ∀T:𝕌'
     ((((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T))
     ⇒ (∀x,y:coSet{i:l}.  (R[x;y] ⇒ (x = y ∈ T)))
     ⇒ (∀x,y:coSet{i:l}.  (R[x;y] ⇒ (x = y ∈ (a:Type × (a ⟶ T))))))
7. R[x;y]
8. T : 𝕌'
9. ((a:Type × (a ⟶ T)) ⊆r T) ∧ (corec(T.a:Type × (a ⟶ T)) ⊆r T)
10. (∀x,y:coSet{i:l}.  (R[x;y] ⇒ (x = y ∈ T))) ⇒ (∀x,y:coSet{i:l}.  (R[x;y] ⇒ (x = y ∈ (a:Type × (a ⟶ T)))))
⊢ (∀x,y:corec(T.a:Type × (a ⟶ T)).  (R[x;y] ⇒ (x = y ∈ T)))
⇒ (∀x,y:corec(T.a:Type × (a ⟶ T)).  (R[x;y] ⇒ (x = y ∈ (a:Type × (a ⟶ T)))))
BY
{ RepeatFor 3 (ParallelLast) }

---

Latex:

---

Latex:

1.  corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \mmember{}  \mBbbU{}'
2.  \mforall{}[R:corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  {}\mrightarrow{}  corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  {}\mrightarrow{}  \mBbbP{}']
          \mforall{}[x,y:corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))].    x  =  y  supposing  R[x;y] 
          supposing  F-bisimulation\{i':l\}(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T);  x,y.R[x;y])
3.  x  :  coSet\{i:l\}
4.  y  :  coSet\{i:l\}
5.  R  :  coSet\{i:l\}  {}\mrightarrow{}  coSet\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
6.  \mforall{}T:\mBbbU{}'
          ((((a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T)  \mwedge{}  (coSet\{i:l\}  \msubseteq{}r  T))
          {}\mRightarrow{}  (\mforall{}x,y:coSet\{i:l\}.    (R[x;y]  {}\mRightarrow{}  (x  =  y)))
          {}\mRightarrow{}  (\mforall{}x,y:coSet\{i:l\}.    (R[x;y]  {}\mRightarrow{}  (x  =  y))))
7.  R[x;y]
8.  T  :  \mBbbU{}'
9.  ((a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T)  \mwedge{}  (corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T)
10.  (\mforall{}x,y:coSet\{i:l\}.    (R[x;y]  {}\mRightarrow{}  (x  =  y)))  {}\mRightarrow{}  (\mforall{}x,y:coSet\{i:l\}.    (R[x;y]  {}\mRightarrow{}  (x  =  y)))
\mvdash{}  (\mforall{}x,y:corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T)).    (R[x;y]  {}\mRightarrow{}  (x  =  y)))
{}\mRightarrow{}  (\mforall{}x,y:corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T)).    (R[x;y]  {}\mRightarrow{}  (x  =  y)))


By

---

Latex:
RepeatFor  3  (ParallelLast)

---

Home Index