---

Step * of Lemma coSet-equality

∀x,y:coSet{i:l}.
  (x = y ∈ coSet{i:l} ⇐⇒ ∃R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∧ R[x;y]))
BY
{ ((InstLemma `corec_wf` [⌜parm{i'}⌝;⌜λ2T.a:Type × (a ⟶ T)⌝]⋅ THENA Auto)
   THEN (InstLemma `coinduction-principle` [⌜parm{i'}⌝;⌜λ2W.a:Type × (a ⟶ W)⌝]⋅ THENA (Auto THEN D 0 THEN Auto))
   ) }

1
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])
⊢ ∀x,y:coSet{i:l}.
    (x = y ∈ coSet{i:l} ⇐⇒ ∃R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'. (coSet-bisimulation{i:l}(x,y.R[x;y]) ∧ R[x;y]))

---

Latex:

---

Latex:
\mforall{}x,y:coSet\{i:l\}.
    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \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:
((InstLemma  `corec\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `coinduction-principle`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}W.a:Type  \mtimes{}  (a  {}\mrightarrow{}  W)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Auto)
              )
  )

---

Home Index