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