Step
*
of Lemma
fix_wf_coSet
∀[G:⋂W:𝕌'. (W ⟶ (T:Type × (T ⟶ W)))]. (fix(G) ∈ coSet{i:l})
BY
{ Auto }
Latex:
Latex:
\mforall{}[G:\mcap{}W:\mBbbU{}'.  (W  {}\mrightarrow{}  (T:Type  \mtimes{}  (T  {}\mrightarrow{}  W)))].  (fix(G)  \mmember{}  coSet\{i:l\})
By
Latex:
Auto
Home
Index