---

Step * of Lemma fix_wf_coW

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[G:⋂W:𝕌'. (W ⟶ (a:A × (B[a] ⟶ W)))].  (fix(G) ∈ coW(A;a.B[a]))
BY
{ ((Auto THEN SubsumeC ⌜corec(W.a:A × (B[a] ⟶ W))⌝⋅) THEN Auto) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. G : ⋂W:𝕌'. (W ⟶ (a:A × (B[a] ⟶ W)))
4. fix(G) = fix(G) ∈ corec(W.a:A × (B[a] ⟶ W))
⊢ corec(W.a:A × (B[a] ⟶ W)) ⊆r coW(A;a.B[a])

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[G:\mcap{}W:\mBbbU{}'.  (W  {}\mrightarrow{}  (a:A  \mtimes{}  (B[a]  {}\mrightarrow{}  W)))].    (fix(G)  \mmember{}  coW(A;a.B[a]))


By

---

Latex:
((Auto  THEN  SubsumeC  \mkleeneopen{}corec(W.a:A  \mtimes{}  (B[a]  {}\mrightarrow{}  W))\mkleeneclose{}\mcdot{})  THEN  Auto)

---

Home Index