---

Step * of Lemma MultiTreeco-ext

∀[T:Type]
  MultiTreeco(T) ≡ lbl:Atom × if lbl =a "Node" then labels:{L:Atom List| 0 < ||L||}  × ({a:Atom| (a ∈ labels)}  ⟶ Multi\000CTreeco(T))
                              if lbl =a "Leaf" then T
                              else Void
                              fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    MultiTreeco(T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Node"
                                                                then  labels:\{L:Atom  List|  0  <  ||L||\} 
                                                                          \mtimes{}  (\{a:Atom|  (a  \mmember{}  labels)\}    {}\mrightarrow{}  MultiTreeco(T))
                                                            if  lbl  =a  "Leaf"  then  T
                                                            else  Void
                                                            fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index