---

Step * 1 2 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} ⟶ ℙ'. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∧ R[x;y])
⊢ x = y ∈ coSet{i:l}
BY
{ (ExRepD THEN InstHyp [⌜R⌝;⌜x⌝;⌜y⌝] 2⋅ THEN Auto) }

1
.....antecedent..... 
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. coSet-bisimulation{i:l}(x,y.R[x;y])
7. R[x;y]
⊢ F-bisimulation{i':l}(T.a:Type × (a ⟶ T); x,y.R[x;y])

---

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.  \mexists{}R:coSet\{i:l\}  {}\mrightarrow{}  coSet\{i:l\}  {}\mrightarrow{}  \mBbbP{}'.  (coSet-bisimulation\{i:l\}(x,y.R[x;y])  \mwedge{}  R[x;y])
\mvdash{}  x  =  y


By

---

Latex:
(ExRepD  THEN  InstHyp  [\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  2\mcdot{}  THEN  Auto)

---

Home Index