---

Step * of Lemma RankEx1co-ext

∀[T:Type]
  RankEx1co(T) ≡ lbl:Atom × if lbl =a "Leaf" then T
                            if lbl =a "Prod" then RankEx1co(T) × RankEx1co(T)
                            if lbl =a "ProdL" then T × RankEx1co(T)
                            if lbl =a "ProdR" then RankEx1co(T) × T
                            if lbl =a "List" then RankEx1co(T) List
                            else Void
                            fi 
BY
{ ProveCoDatatypeExt }

---

Latex:


\mforall{}[T:Type]
    RankEx1co(T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "Leaf"  then  T
                                                        if  lbl  =a  "Prod"  then  RankEx1co(T)  \mtimes{}  RankEx1co(T)
                                                        if  lbl  =a  "ProdL"  then  T  \mtimes{}  RankEx1co(T)
                                                        if  lbl  =a  "ProdR"  then  RankEx1co(T)  \mtimes{}  T
                                                        if  lbl  =a  "List"  then  RankEx1co(T)  List
                                                        else  Void
                                                        fi 


By

ProveCoDatatypeExt

---

Home Index