---

Step * of Lemma MMTreeco-ext

∀[T:Type]. MMTreeco(T) ≡ lbl:Atom × if lbl =a "Leaf" then T if lbl =a "Node" then MMTreeco(T) List List else Void fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    MMTreeco(T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Leaf"  then  T
                                                      if  lbl  =a  "Node"  then  MMTreeco(T)  List  List
                                                      else  Void
                                                      fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index