---

{ [T:Type]. [g:LabeledGraph(T)].  (lg-append(lg-nil();g) ~ g) }

{ Proof }

---

Definitions occuring in Statement :  lg-append: lg-append(g1;g2),  lg-nil: lg-nil(),  labeled-graph: LabeledGraph(T),  uall: [x:A]. B[x],  universe: Type,  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  lg-append: lg-append(g1;g2),  lg-nil: lg-nil(),  append: as @ bs,  lg-size: lg-size(g),  length: ||as||,  ycomb: Y,  member: t  T,  all: x:A. B[x],  implies: P  Q,  map: map(f;as),  spreadn: spread3,  labeled-graph: LabeledGraph(T),  int_seg: {i..j},  nat: ,  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T}
Lemmas :  labeled-graph_wf,  lg-size_wf,  subtype_rel_list,  int_seg_wf,  nat_wf,  subtype_rel_simple_product,  subtype_rel_self,  nat_properties,  subtype_base_sq,  int_subtype_base

---

\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].    (lg-append(lg-nil();g)  \msim{}  g)


Date html generated: 2011_08_16-PM-06_36_25
Last ObjectModification: 2011_06_20-AM-01_55_57

Home Index