---

Step * of Lemma corec-subtype-coSet

corec(T.a:Type × (a ⟶ T)) ⊆r coSet{i:l}
BY
{ (((InstLemma `coW-corec` [⌜Type⌝;⌜λ2x.x⌝]⋅ THENA Auto) THEN Fold `coSet` (-1)) THEN Auto) }

---

Latex:

---

Latex:
corec(T.a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  coSet\{i:l\}


By

---

Latex:
(((InstLemma  `coW-corec`  [\mkleeneopen{}Type\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Fold  `coSet`  (-1))  THEN  Auto)

---

Home Index