---

Step * of Lemma treeco-ext

∀[E:Type]. treeco(E) ≡ lbl:Atom × if lbl =a "leaf" then E if lbl =a "node" then left:treeco(E) × treeco(E) else Void fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[E:Type]
    treeco(E)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "leaf"  then  E
                                                  if  lbl  =a  "node"  then  left:treeco(E)  \mtimes{}  treeco(E)
                                                  else  Void
                                                  fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index