---

Step * of Lemma fix_wf_coSet_system_weak

∀[I:𝕌']. ∀[G:⋂C:𝕌'. ((I ⟶ C) ⟶ I ⟶ (T:Type × (T ⟶ C)))].  (fix(G) ∈ I ⟶ coSet{i:l})
BY
{ (InstLemma `fix_wf_coSet_system` [] THEN RepeatFor 2 (ParallelLast')) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `fix\_wf\_coSet\_system`  []  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index