---

Step * of Lemma fix_wf_coSet_system

∀[I:𝕌']. ∀[G:⋂C:{C:𝕌'| ((T:Type × (T ⟶ C)) ⊆r C) ∧ (coSet{i:l} ⊆r C)} . ((I ⟶ C) ⟶ I ⟶ (T:Type × (T ⟶ C)))].
  (fix(G) ∈ I ⟶ coSet{i:l})
BY
{ (Auto THEN (InstLemma `corec_wf` [⌜parm{i'}⌝;⌜λ2C.T:Type × (T ⟶ C)⌝]⋅ THENA Auto)) }

1
1. I : 𝕌'
2. G : ⋂C:{C:𝕌'| ((T:Type × (T ⟶ C)) ⊆r C) ∧ (coSet{i:l} ⊆r C)} . ((I ⟶ C) ⟶ I ⟶ (T:Type × (T ⟶ C)))
3. corec(T.T@0:Type × (T@0 ⟶ T)) ∈ 𝕌'
⊢ fix(G) ∈ I ⟶ coSet{i:l}

---

Latex:

---

Latex:
\mforall{}[I:\mBbbU{}'].  \mforall{}[G:\mcap{}C:\{C:\mBbbU{}'|  ((T:Type  \mtimes{}  (T  {}\mrightarrow{}  C))  \msubseteq{}r  C)  \mwedge{}  (coSet\{i:l\}  \msubseteq{}r  C)\} 
                              ((I  {}\mrightarrow{}  C)  {}\mrightarrow{}  I  {}\mrightarrow{}  (T:Type  \mtimes{}  (T  {}\mrightarrow{}  C)))].
    (fix(G)  \mmember{}  I  {}\mrightarrow{}  coSet\{i:l\})


By

---

Latex:
(Auto  THEN  (InstLemma  `corec\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}C.T:Type  \mtimes{}  (T  {}\mrightarrow{}  C)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index