Nuprl Lemma : manames-overlap-case_wf
∀[T:Type]. ∀[x,y:T]. ∀[nms1,nms2:MaName List]. (if nms1 and nms2 overlap then x else y fi ∈ T)
Proof
Definitions occuring in Statement :
manames-overlap-case: if nms1 and nms2 overlap then x else y fi,
MaName: MaName,
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
branch_wf2,
l_disjoint_wf,
MaName_wf,
all_wf,
list_wf,
decidable_wf,
not_wf
\mforall{}[T:Type]. \mforall{}[x,y:T]. \mforall{}[nms1,nms2:MaName List]. (if nms1 and nms2 overlap then x else y fi \mmember{} T)
Date html generated:
2015_07_17-AM-09_15_02
Last ObjectModification:
2015_01_28-AM-07_53_48
Home
Index