Nuprl Lemma : list_contained-in_wf
[T:Type]. [L1,L2:T List]. (list_contained-in(L1;L2;T) 
)
Proof not projected
Definitions occuring in Statement :
list_contained-in: list_contained-in(L1;L2;T),
uall: [x:A]. B[x],
prop: ,
member: t T,
list: type List,
universe: Type
Definitions :
lambda: 
x.A[x],
l_member: (x l),
so_lambda: 
x.t[x],
function: x:A 
B[x],
all: x:A. B[x],
list_all: list_all(x.P[x];l),
prop: ,
list_contained-in: list_contained-in(L1;L2;T),
universe: Type,
axiom: Ax,
list: type List,
isect: 
x:A. B[x],
member: t T,
equal: s = t,
uall: [x:A]. B[x]
Lemmas :
list_all_wf,
l_member_wf
\mforall{}[T:Type]. \mforall{}[L1,L2:T List]. (list\_contained-in(L1;L2;T) \mmember{} \mBbbP{})
Date html generated:
2011_10_20-PM-04_50_24
Last ObjectModification:
2011_05_13-PM-05_41_01
Home
Index