---

Step * 1 1 1 of Lemma coSet-equality2


1. x : coSet{i:l}
2. y : coSet{i:l}
3. ∀T:𝕌'. ((((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T)) ⇒ (x = y ∈ T) ⇒ (x = y ∈ (a:Type × (a ⟶ T))))
⊢ ∃R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∧ R[x;y])
BY
{ ((D 0 With ⌜λa,b. ((a = x ∈ coSet{i:l}) ∧ (b = y ∈ coSet{i:l}))⌝  THENA Auto) THEN RepUR ``so_apply`` 0 THEN Auto) }

1
1. x : coSet{i:l}
2. y : coSet{i:l}
3. ∀T:𝕌'. ((((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T)) ⇒ (x = y ∈ T) ⇒ (x = y ∈ (a:Type × (a ⟶ T))))
⊢ coSet-bisimulation{i:l}(x@0,y@0.(x@0 = x ∈ coSet{i:l}) ∧ (y@0 = y ∈ coSet{i:l}))

---

Latex:

---

Latex:

1.  x  :  coSet\{i:l\}
2.  y  :  coSet\{i:l\}
3.  \mforall{}T:\mBbbU{}'.  ((((a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T)  \mwedge{}  (coSet\{i:l\}  \msubseteq{}r  T))  {}\mRightarrow{}  (x  =  y)  {}\mRightarrow{}  (x  =  y))
\mvdash{}  \mexists{}R:coSet\{i:l\}  {}\mrightarrow{}  coSet\{i:l\}  {}\mrightarrow{}  \mBbbP{}'.  (coSet-bisimulation\{i:l\}(x,y.R[x;y])  \mwedge{}  R[x;y])


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}a,b.  ((a  =  x)  \mwedge{}  (b  =  y))\mkleeneclose{}    THENA  Auto)  THEN  RepUR  ``so\_apply``  0  THEN  Auto)

---

Home Index