---

{ [x,y:Top]. [nms:MaName List].
    (if [] and nms overlap then x else y fi ~ y) }

{ Proof }

---

Definitions occuring in Statement :  manames-overlap-case: if nms1 and nms2 overlap then x else y fi,  MaName: MaName,  uall: [x:A]. B[x],  top: Top,  nil: [],  list: type List,  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  manames-overlap-case: if nms1 and nms2 overlap then x else y fi,  member: t  T,  branch: if p:P then A[p] else B fi ,  all: x:A. B[x],  prop: ,  implies: P  Q,  decidable: Dec(P),  or: P  Q,  not: A,  false: False
Lemmas :  MaName_wf,  decidable_wf,  l_disjoint_wf,  l_disjoint_nil,  top_wf

---

\mforall{}[x,y:Top].  \mforall{}[nms:MaName  List].    (if  []  and  nms  overlap  then  x  else  y  fi  \msim{}  y)


Date html generated: 2011_08_10-AM-07_52_21
Last ObjectModification: 2011_06_18-AM-08_14_33

Home Index