---

Step * of Lemma l_tree-ext

∀[L,T:Type].
  l_tree(L;T) ≡ lbl:Atom × if lbl =a "leaf" then L
                           if lbl =a "node" then val:T × left_subtree:l_tree(L;T) × l_tree(L;T)
                           else Void
                           fi 
BY
{ ProveDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[L,T:Type].
    l\_tree(L;T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "leaf"  then  L
                                                      if  lbl  =a  "node"  then  val:T  \mtimes{}  left$_{subtree}$:l\_tree\000C(L;T)  \mtimes{}  l\_tree(L;T)
                                                      else  Void
                                                      fi 


By

---

Latex:
ProveDatatypeExt

---

Home Index