Nuprl Lemma : manames-overlap-nil2
∀[x,y:Top]. ∀[nms:MaName List]. (if nms and [] 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,
nil: [],
list: T List,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
all_wf,
list_wf,
MaName_wf,
decidable_wf,
l_disjoint_wf,
nil_wf,
l_disjoint_nil2,
equal_wf,
top_wf
\mforall{}[x,y:Top]. \mforall{}[nms:MaName List]. (if nms and [] overlap then x else y fi \msim{} y)
Date html generated:
2015_07_17-AM-09_15_08
Last ObjectModification:
2015_01_28-AM-07_53_44
Home
Index