Nuprl Lemma : sv-list-equal
∀T:Type. ∀L1,L2:T List. ∀x:T.
(single-valued-list(L1;T)
⇒ single-valued-list(L2;T)
⇒ (x ∈ L1)
⇒ (x ∈ L2)
⇒ (||L1|| = ||L2|| ∈ ℤ)
⇒ (L1 = L2 ∈ (T List)))
Proof
Definitions occuring in Statement :
single-valued-list: single-valued-list(L;T),
l_member: (x ∈ l),
length: ||as||,
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
list_extensionality,
select_wf,
sq_stable__le,
select_member,
lelt_wf,
less_than_transitivity1,
le_weakening,
less_than_wf,
nat_wf,
equal_wf,
length_wf,
l_member_wf,
single-valued-list_wf,
list_wf
Latex:
\mforall{}T:Type. \mforall{}L1,L2:T List. \mforall{}x:T.
(single-valued-list(L1;T)
{}\mRightarrow{} single-valued-list(L2;T)
{}\mRightarrow{} (x \mmember{} L1)
{}\mRightarrow{} (x \mmember{} L2)
{}\mRightarrow{} (||L1|| = ||L2||)
{}\mRightarrow{} (L1 = L2))
Date html generated:
2015_07_23-AM-11_25_53
Last ObjectModification:
2015_01_28-PM-11_15_56
Home
Index