---

{ [T:Type]. [g1,g2:LabeledGraph(T)].  (g1  g2  ) }

{ Proof }

---

Definitions occuring in Statement :  lg-contains: g1  g2,  labeled-graph: LabeledGraph(T),  uall: [x:A]. B[x],  prop: ,  member: t  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  prop: ,  lg-contains: g1  g2,  exists: x:A. B[x]
Lemmas :  lg-append_wf,  labeled-graph_wf

---

\mforall{}[T:Type].  \mforall{}[g1,g2:LabeledGraph(T)].    (g1  \msubseteq{}  g2  \mmember{}  \mBbbP{})


Date html generated: 2011_08_16-PM-06_36_31
Last ObjectModification: 2011_06_20-AM-01_56_06

Home Index