---

Step * 1 of Lemma fix_wf_coSet_system


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}
BY
{ (SubsumeC ⌜I ⟶ corec(W.X:Type × (X ⟶ W))⌝⋅
   THENL [((InstLemma `fix_wf_corec_system` [⌜parm{i'}⌝;⌜λ2W.T:Type × (T ⟶ W)⌝;⌜I⌝]⋅ THENA Auto)
           THEN BHyp -1 
           THEN MemTypeCD
           THEN Auto)
         ; Auto]
) }

---

Latex:

---

Latex:

1.  I  :  \mBbbU{}'
2.  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)))
3.  corec(T.T@0:Type  \mtimes{}  (T@0  {}\mrightarrow{}  T))  \mmember{}  \mBbbU{}'
\mvdash{}  fix(G)  \mmember{}  I  {}\mrightarrow{}  coSet\{i:l\}


By

---

Latex:
(SubsumeC  \mkleeneopen{}I  {}\mrightarrow{}  corec(W.X:Type  \mtimes{}  (X  {}\mrightarrow{}  W))\mkleeneclose{}\mcdot{}
  THENL  [((InstLemma  `fix\_wf\_corec\_system`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}W.T:Type  \mtimes{}  (T  {}\mrightarrow{}  W)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  BHyp  -1 
                  THEN  MemTypeCD
                  THEN  Auto)
              ;  Auto]
)

---

Home Index