---

{ [T:Type]. (lg-nil()  LabeledDAG(T)) }

{ Proof }

---

Definitions occuring in Statement :  ldag: LabeledDAG(T),  lg-nil: lg-nil(),  uall: [x:A]. B[x],  member: t  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  ldag: LabeledDAG(T),  is-dag: is-dag(g),  lg-nil: lg-nil(),  all: x:A. B[x],  lg-size: lg-size(g),  implies: P  Q,  length: ||as||,  ycomb: Y,  prop: ,  int_seg: {i..j},  lelt: i  j < k,  and: P  Q,  le: A  B,  not: A,  false: False
Lemmas :  lg-nil_wf,  is-dag_wf,  int_seg_wf

---

\mforall{}[T:Type].  (lg-nil()  \mmember{}  LabeledDAG(T))


Date html generated: 2011_08_16-PM-06_45_44
Last ObjectModification: 2011_06_18-AM-10_57_54

Home Index