---

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

{ Proof }

---

Definitions occuring in Statement :  lg-contains: g1  g2,  labeled-graph: LabeledGraph(T),  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  uimplies: b supposing a,  lg-contains: g1  g2,  exists: x:A. B[x],  member: t  T,  prop: ,  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  implies: P  Q
Lemmas :  labeled-graph_wf,  lg-nil_wf,  lg-append_wf,  lg-nil-append,  lg-append-nil

---

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


Date html generated: 2011_08_16-PM-06_36_52
Last ObjectModification: 2011_06_20-AM-01_56_34

Home Index