Nuprl Lemma : aa_sublist_reflexive
T:Type. l:T List. l 
l
Proof
Definitions occuring in Statement :
all: x:A. B[x],
universe: Type,
sublist: L1 L2
Definitions :
all: x:A. B[x],
member: t 
T,
sublist: L1 L2,
exists: 
x:A. B[x],
and: P 
Q,
subtype: S T,
suptype: suptype(S; T),
so_lambda: 
x.t[x],
increasing: increasing(f;k),
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
int_seg: {i..j
},
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
lelt: i j < k,
prop: 
Lemmas :
int_seg_wf,
length_wf,
and_wf,
increasing_wf,
length_wf_nat,
all_wf,
equal_wf,
select_wf,
non_neg_length
\mforall{}T:Type. \mforall{}l:T List. l \msubseteq{} l
Date html generated:
2013_03_20-AM-09_51_55
Last ObjectModification:
2012_11_27-AM-10_32_13
Home
Index