---

Step * of Lemma coW-corec

∀[A:𝕌']. ∀[B:A ⟶ Type].  coW(A;a.B[a]) ≡ corec(C.a:A × (B[a] ⟶ C))
BY
{ (Auto
   THEN (InstLemma `corec_wf` [⌜parm{i'}⌝;⌜λ2C.a:A × (B[a] ⟶ C)⌝]⋅ THENA Auto)
   THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. A : 𝕌'
2. B : A ⟶ Type
3. corec(T.a:A × (B[a] ⟶ T)) ∈ 𝕌'
4. x : coW(A;a.B[a])
⊢ x ∈ corec(C.a:A × (B[a] ⟶ C))

2
.....subterm..... T:t
1:n
1. A : 𝕌'
2. B : A ⟶ Type
3. corec(T.a:A × (B[a] ⟶ T)) ∈ 𝕌'
4. x : corec(C.a:A × (B[a] ⟶ C))
⊢ x ∈ coW(A;a.B[a])

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].    coW(A;a.B[a])  \mequiv{}  corec(C.a:A  \mtimes{}  (B[a]  {}\mrightarrow{}  C))


By

---

Latex:
(Auto
  THEN  (InstLemma  `corec\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}C.a:A  \mtimes{}  (B[a]  {}\mrightarrow{}  C)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index